Typed operational semantics

1. T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, 1993.

   Google Scholar 

2. H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North Holland, revised edition, 1984.

   Google Scholar 

3. H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbai, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1991.

   Google Scholar 

4. T. Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.

   Google Scholar 

5. T. Coquand and J. Gallier. A proof of strong normalization for the theory of constructions using a Kripke-like interpretation. In Workshop on Logical Frameworks-Preliminary Proceedings, 1990.

   Google Scholar 

6. H. Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, Sept. 1993.

   Google Scholar 

7. H. Goguen. The metatheory of UTT. Submitted to Proceedings of BRA Workshop on Types for Proofs and Programs, 1994.

   Google Scholar 

8. H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, Aug. 1994.

   Google Scholar 

9. Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, Nov. 1990.

   Google Scholar 

10. Z. Luo. Computation and Reasoning. Oxford University Press, 1994.

    Google Scholar 

11. P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. Rose and J. C. Shepherdson, editors, Logic Colloqium 1973, pages 73–118, 1975.

    Google Scholar 

12. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

    Google Scholar 

13. J. McKinna and R. Pollack. Pure type systems formalized. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 289–305. Springer-Verlag, LNCS 664, Mar. 1993.

    Google Scholar 

14. J. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. North Holland, 1990.

    Google Scholar 

15. A. Salvesen. The Church-Rosser property for pure type systems with βη-reduction, Nov. 1991. Unpublished manuscript.

    Google Scholar 

16. W. W. Tait. Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic, 32, 1967.

    Google Scholar 

17. L. van Benthem Jutting, J. McKinna, and R. Pollack. Typechecking in pure type systems. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programming. Springer-Verlag, 1993.

    Google Scholar 

Download references