Substitution up to isomorphism
Diagrammes, Tome 23 (1990), pp. 43-66. 
@article{DIA_1990__23__43_0,
     author = {Curien, P.-L.},
     title = {Substitution up to isomorphism},
     journal = {Diagrammes},
     pages = {43--66},
     publisher = {Universit\'e Paris 7, Unit\'e d'enseignement et de recherche de math\'ematiques},
     volume = {23},
     year = {1990},
     mrnumber = {1082997},
     zbl = {0715.03029},
     language = {en},
     url = {http://archive.numdam.org/item/DIA_1990__23__43_0/}
}
TY  - JOUR
AU  - Curien, P.-L.
TI  - Substitution up to isomorphism
JO  - Diagrammes
PY  - 1990
SP  - 43
EP  - 66
VL  - 23
PB  - Université Paris 7, Unité d'enseignement et de recherche de mathématiques
UR  - http://archive.numdam.org/item/DIA_1990__23__43_0/
LA  - en
ID  - DIA_1990__23__43_0
ER  - 
%0 Journal Article
%A Curien, P.-L.
%T Substitution up to isomorphism
%J Diagrammes
%D 1990
%P 43-66
%V 23
%I Université Paris 7, Unité d'enseignement et de recherche de mathématiques
%U http://archive.numdam.org/item/DIA_1990__23__43_0/
%G en
%F DIA_1990__23__43_0
Curien, P.-L. Substitution up to isomorphism. Diagrammes, Tome 23 (1990), pp. 43-66. http://archive.numdam.org/item/DIA_1990__23__43_0/

[ACCL] M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit Substitutions, in Proc. ACM Principles of Programming Languages, San Francisco ( 1990). | MR

[Brui] N. De Bruijn, Lambda-calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, Indag Math. 34 ( 1972). | Zbl

[Cart] J. Cartmell, Generalized Algebraic Theories and Contextual Categories, Thesis, Oxford ( 1978).

[Coq] T. Coquand, Metamathematical Investigations of a Calculus of Constructions, Technical Report, Cambridge University ( 1987).

[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). | MR | Zbl

[CouCurMau] G. Cousineau, P.-L. Curien, M. Mauny, The Categorical Abstract Machine, Science of Computer Programming 8, pp. 173-202 ( 1987). | MR | Zbl

[CuGhe] P.-L. Curien, G. Ghelli, Coherence of Subsumption, accepted at CAAP 90, Copenhaguen. | Zbl

[Cur1] P.-L. Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman ( 1986). | MR | Zbl

[Cur2] P.-L. Curien, α-conversion, Conditions on Variables and Categorical Logic, Studia Logica, to appear. | MR | Zbl

[Ehr] T. Ehrhard, A Categorical Semantics of Constructions, LICS 88, Edinburgh ( 1988).

[Guit] R. Guitart, Relations et Carrés Exacts, Annales Sci. Math, du Québec, Vol. IV , No2, pp. 103-125 ( 1980). | MR | Zbl

[HarLa] T. Hardin, A. Laville, Proof of Termination of the Rewriting System Subst on CCL, Theoret. Comput. Sci. 46, pp. 305-312 ( 1986). | MR | Zbl

[HueOp] G. Huet, D. Oppen, Equations and Rewrite Rules: a Survey, in FormalLanguages, Perspectives and Open Problems, R. Book ed., Academie Press ( 1980).

[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). | MR | Zbl

[Jac] B. Jacobs, Some Notes on Fibred Categories and the Semantics of Dependent Types, Technical Report 22/89, Universita di Pisa, ( 1989).

[Laf] Y. Lafont, Personal communication.

[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. | MR | Zbl

[Law] W. Lawvere, Adjointness in Foundations, Dialectica 23(3/4) ( 1969). | Zbl

[MacLaPar] S. Mac Lane, R. Paré, Coherence for Bicategories and Indexed Categories, Journal of Pure and Applied Logic 37, 59-80 ( 1985). | MR | Zbl

[Mar] P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis ( 1984). | MR | Zbl

[MeyRein] A. Meyer, M. Reinhold, Type' is not a Type, Proc. LICS 86.

[Ob] A. Obtulowicz, Categorical and Algebraic Aspects of Martin-Löf Type Theory, Studia Logica, to appear. | MR | Zbl

[Pow] A. Power, A 2-categorical Pasting Theorem, Journal of Algebra, to appear. | Zbl

[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 .

[Se] R. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. 95 ( 1984). | MR | Zbl

[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). | Zbl

[Tay] P. Taylor, Recursive Domains, Indexed Category Theory and Polymorphism, PhD Thesis, University of Cambridge ( 1986).