Substitution up to isomorphism

P.-L. Curien

Diagrammes (1990)

  • Volume: 23, page 43-66
  • ISSN: 0224-3911

How to cite

top

Curien, P.-L.. "Substitution up to isomorphism." Diagrammes 23 (1990): 43-66. <http://eudml.org/doc/91749>.

@article{Curien1990,
author = {Curien, P.-L.},
journal = {Diagrammes},
keywords = {categorical semantics of dependent types; coherence problems; modelling of substitution in types by pullbacks; interpretation of dependent types in a locally Cartesian closed category},
language = {eng},
pages = {43-66},
publisher = {Université Paris 7, Unité d'enseignement et de recherche de mathématiques},
title = {Substitution up to isomorphism},
url = {http://eudml.org/doc/91749},
volume = {23},
year = {1990},
}

TY - JOUR
AU - Curien, P.-L.
TI - Substitution up to isomorphism
JO - Diagrammes
PY - 1990
PB - Université Paris 7, Unité d'enseignement et de recherche de mathématiques
VL - 23
SP - 43
EP - 66
LA - eng
KW - categorical semantics of dependent types; coherence problems; modelling of substitution in types by pullbacks; interpretation of dependent types in a locally Cartesian closed category
UR - http://eudml.org/doc/91749
ER -

References

top
  1. [ACCL] M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit Substitutions, in Proc. ACM Principles of Programming Languages, San Francisco ( 1990). MR1140338
  2. [Brui] N. De Bruijn, Lambda-calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, Indag Math. 34 ( 1972). Zbl0253.68007
  3. [Cart] J. Cartmell, Generalized Algebraic Theories and Contextual Categories, Thesis, Oxford ( 1978). 
  4. [Coq] T. Coquand, Metamathematical Investigations of a Calculus of Constructions, Technical Report, Cambridge University ( 1987). 
  5. [CoqEhr] T. Coquand, T. Ehrhard, An Equational Presentation of Higher-Order Logic, Proc. 2nd Conf. on Category Theory and Computer Science, Lecture Notes in Comput. Sci. 283 ( 1987). Zbl0643.03050MR925223
  6. [CouCurMau] G. Cousineau, P.-L. Curien, M. Mauny, The Categorical Abstract Machine, Science of Computer Programming 8, pp. 173-202 ( 1987). Zbl0634.68078MR896255
  7. [CuGhe] P.-L. Curien, G. Ghelli, Coherence of Subsumption, accepted at CAAP 90, Copenhaguen. Zbl0759.03009
  8. [Cur1] P.-L. Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman ( 1986). Zbl0643.68004MR840874
  9. [Cur2] P.-L. Curien, α-conversion, Conditions on Variables and Categorical Logic, Studia Logica, to appear. Zbl0701.03036MR1059246
  10. [Ehr] T. Ehrhard, A Categorical Semantics of Constructions, LICS 88, Edinburgh ( 1988). 
  11. [Guit] R. Guitart, Relations et Carrés Exacts, Annales Sci. Math, du Québec, Vol. IV , No2, pp. 103-125 ( 1980). Zbl0495.18008MR599050
  12. [HarLa] T. Hardin, A. Laville, Proof of Termination of the Rewriting System Subst on CCL, Theoret. Comput. Sci. 46, pp. 305-312 ( 1986). Zbl0618.68031MR869211
  13. [HueOp] G. Huet, D. Oppen, Equations and Rewrite Rules: a Survey, in FormalLanguages, Perspectives and Open Problems, R. Book ed., Academie Press ( 1980). 
  14. [HyPit] M. Hyland, A. Pitts, The Theory of Constructions: Categorical Semantics and Topos-theoretic Models, Proc. Conf. on Categories in Computer Science and Logic, to appear as Contemporary Mathematics volume, Boulder ( 1987). Zbl0721.03048MR925222
  15. [Jac] B. Jacobs, Some Notes on Fibred Categories and the Semantics of Dependent Types, Technical Report 22/89, Universita di Pisa, ( 1989). 
  16. [Laf] Y. Lafont, Personal communication. 
  17. [Lam] F. Lamarche, A Simple Model of the Theory of Constructions, in J. Gray and A. Scedrov (eds), Categories in Computer Science and Logic, Contemporary Mathematics 92, 1989. Zbl0683.18006MR1003200
  18. [Law] W. Lawvere, Adjointness in Foundations, Dialectica 23(3/4) ( 1969). Zbl0341.18002
  19. [MacLaPar] S. Mac Lane, R. Paré, Coherence for Bicategories and Indexed Categories, Journal of Pure and Applied Logic 37, 59-80 ( 1985). Zbl0567.18003MR794793
  20. [Mar] P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis ( 1984). Zbl0571.03030MR769301
  21. [MeyRein] A. Meyer, M. Reinhold, Type' is not a Type, Proc. LICS 86. 
  22. [Ob] A. Obtulowicz, Categorical and Algebraic Aspects of Martin-Löf Type Theory, Studia Logica, to appear. Zbl0714.03050MR1059245
  23. [Pow] A. Power, A 2-categorical Pasting Theorem, Journal of Algebra, to appear. Zbl0698.18005
  24. [Rod]E.G. Rodeja F., editor of various technical reports of theDepartamento of Algebra y Fundamentos del Universidad de Santiago de Compostela, starting withTeoria de Triples by J.R. Caruncho Castro . 
  25. [Se] R. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. 95 ( 1984). Zbl0539.03048MR727078
  26. [Stre] T. Streicher, Correctness and Completeness of a Semantics of the Calculus of Constructions with Respect to Interpretation in Doctrines of Constructions, Thesis, Universität Passau ( 1988). Zbl0684.03025
  27. [Tay] P. Taylor, Recursive Domains, Indexed Category Theory and Polymorphism, PhD Thesis, University of Cambridge ( 1986). 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.