A Short Proof of the Strong Normalization of the Simply Typed lambda mi-calculus

• Autorzy: David R. , Nour K.
• Języki publikacji: PL

Abstrakty

EN

We give an elementary and purely arithmetical proof of the strong normalization of Parigot's simply typed lambda-calculus.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Schedae Informaticae
• Rocznik: 2003
• Tom: Vol. 12
• Strony: 27--33
• Opis fizyczny: Bibliogr. 8 poz.

Twórcy

autor

David R.

• LAMA - Equipe de Logique Universite de Chambery, 73376 Le Bourget du Lac

autor

Nour K.

• LAMA - Equipe de Logique Universite de Chambery, 73376 Le Bourget du Lac

Bibliografia

• [1] Groote de P.; Strong normalization of classical natural deduction with disfunction, TLCA’01, Lecture Notes in Computer Science. Springer-Verlag, Vol. 2044, 2001, pp. 182-196.
• [2] David R.; Normalization without reducibility, Annals of Pure and Applied Logic, Vol. 107, 2001, pp. 121-130.
• [3] Joachimski F., Matthes R.; Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Godel’s T, Arch. Math. Logic, Vol. 42, 2003, pp. 59-87.
• [4] Levy J.J.; Reductions correctes et optimales dans le lambda-calcul, Ph.D. thesis, Paris VII, 1978.
• [5] Parigot M.; λμ-calculus: An algorithm interpretation of classical natural deduction, Lecture Notes in Artificial Intelligence, Springer Verlag, Vol. 624, 1992, pp. 190-201.
• [6] Parigot M.; Proofs of strong normalization for second order classical natural deduction, Journal of Symbolic Logic, Vol. 62(4), 1997, pp. 1461-1479.
• [7] Rehof N.J., Sorensen M.H.; The X λΔ-calculus. TACS'94, Lecture Notes in Com¬puter Science, Springer-Verlag, Vol. 789, 1994, pp. 516-542.
• [8] Daalen van D.; The language theory of Automath, Ph.D. thesis, Eindhoven 1977.