Normalization for typed lambda calculi with explicit substitution

1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.

   MathSciNet  Google Scholar 

2. P.-L. Curien, T. Hardin, and A. Ríos. Strong normalisation of substitutions. In I.M. Havel and V. Koubek, editors, Mathematical Foundations of Computer Science 1992, pages 209–217. Lecture Notes in Computer Science No. 629, Berlin, Heidelberg, New York, 1992.

   Google Scholar 

3. N.G. De Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Math, 34:381–392, 1972.

   Google Scholar 

4. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. Cambridge University Press, Cambridge, 1989.

   Google Scholar 

5. Thérèse Hardin and Alain Laville. Proof of termination of the rewriting system Subst on CCL. Theoretical Computer Science, 46:305–312, 1986.

   Article  MathSciNet  Google Scholar 

6. György E. Révész. Lambda-calculus, combinators and functional programming. Number 4 in Cambridge tracts in theoretical computer science. Cambridge University Press, 1988.

   Google Scholar 

7. Eike Ritter. Categorical Abstract Machines for Higher-Order Lambda Calculi.PhD thesis, University of Cambridge, 1992. Also available as Technical Report No. 297.

   Google Scholar 

8. W. W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor, Logic Colloquium, pages 240–251. LNM 453, Springer Verlag, 1975.

   Google Scholar 

Download references