@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://www.numdam.org/item/DIA_1990__23__43_0/} }
Curien, P.-L. Substitution up to isomorphism. Diagrammes, Volume 23 (1990), pp. 43-66. http://www.numdam.org/item/DIA_1990__23__43_0/
[ACCL] Explicit Substitutions, in Proc. ACM Principles of Programming Languages, San Francisco ( 1990). | MR
, , , ,[Brui] Lambda-calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, Indag Math. 34 ( 1972). | Zbl
,[Cart] Generalized Algebraic Theories and Contextual Categories, Thesis, Oxford ( 1978).
,[Coq] Metamathematical Investigations of a Calculus of Constructions, Technical Report, Cambridge University ( 1987).
,[CoqEhr] 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] The Categorical Abstract Machine, Science of Computer Programming 8, pp. 173-202 ( 1987). | MR | Zbl
, , ,[CuGhe] Coherence of Subsumption, accepted at CAAP 90, Copenhaguen. | Zbl
, ,[Cur1] Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman ( 1986). | MR | Zbl
,[Cur2] Conditions on Variables and Categorical Logic, Studia Logica, to appear. | MR | Zbl
, α-conversion,[Ehr] A Categorical Semantics of Constructions, LICS 88, Edinburgh ( 1988).
,[Guit] Relations et Carrés Exacts, Annales Sci. Math, du Québec, Vol. IV , No2, pp. 103-125 ( 1980). | MR | Zbl
,[HarLa] Proof of Termination of the Rewriting System Subst on CCL, Theoret. Comput. Sci. 46, pp. 305-312 ( 1986). | MR | Zbl
, ,[HueOp] Equations and Rewrite Rules: a Survey, in FormalLanguages, Perspectives and Open Problems, R. Book ed., Academie Press ( 1980).
, ,[HyPit] 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] Some Notes on Fibred Categories and the Semantics of Dependent Types, Technical Report 22/89, Universita di Pisa, ( 1989).
,[Laf] Personal communication.
,[Lam] 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] Adjointness in Foundations, Dialectica 23(3/4) ( 1969). | Zbl
,[MacLaPar] Coherence for Bicategories and Indexed Categories, Journal of Pure and Applied Logic 37, 59-80 ( 1985). | MR | Zbl
, ,[Mar] Intuitionistic Type Theory, Bibliopolis ( 1984). | MR | Zbl
,[MeyRein] Type' is not a Type, Proc. LICS 86.
, ,[Ob] Categorical and Algebraic Aspects of Martin-Löf Type Theory, Studia Logica, to appear. | MR | Zbl
,[Pow] 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 .
[Se] Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. 95 ( 1984). | MR | Zbl
,[Stre] 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] Recursive Domains, Indexed Category Theory and Polymorphism, PhD Thesis, University of Cambridge ( 1986).
,