Categorical reconstruction of a reduction free normalization proof

1. Ulrich Berger. Personal email to Thomas Streicher, April 1994.

   Google Scholar 

2. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 202–211, 1991.

   Google Scholar 

3. Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Preliminary Proceedings of the 1993 TYPES Workshop, Nijmegen (accepted for publication in Mathematical Structures in Computer Science), 1993.

   Google Scholar 

4. Thierry Coquand. An algorithm for testing conversion in type theory. In Logical Frameworks. Cambridge University Press, 1991.

   Google Scholar 

5. Catarina Coquand. From Semantics to Rules: a Machine Assisted Analysis. In Börger, Gurevich, and Meinke, editors, CSL'93, pages 91–105. Springer-Verlag, LNCS 832, 1994.

   Google Scholar 

6. Neil Ghani. Βη-equality for coproducts. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculi and Applications, number 902 in LNCS, pages 171–185, 1995.

   Google Scholar 

7. Gérard Huet and Amokrane SaÏbi. Constructive category theory. In Peter Dybjer and Randy Pollack, editors, Informal proceedings of the joint CLICS-TYPES workshop on categories and type theory, 1995.

   Google Scholar 

8. Saul A. Kripke. Semantical analysis of intutionistic logic I. In J.N. Crossley and M.A.E. Dummett, editors, Formal systems and recursive functions. North Holland, 1965.

   Google Scholar 

9. Joachim Lambek and Phil Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986.

   Google Scholar 

10. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium 1973, pages 73–118, Amsterdam, 1975. North-Holland Publishing Company.

    Google Scholar 

11. John C. Mitchell and Eugenio Moggi. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic, 51:99–124, 1991.

    Google Scholar 

12. Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. An Introduction. Oxford University Press, 1990.

    Google Scholar 

13. A. S. Troelstra and D. van Dalen. Constructivism in Mathematics. An Introduction, volume II. North-Holland, 1988.

    Google Scholar 

Download references