A general method for proving the normalization theorem for first and second order typed λ-calculi

Autor:	Venanzio Capretta, Silvio Valentini
Rok vydání:	1999
Předmět:	Algebra Mathematics (miscellaneous) Simply typed lambda calculus System F Calculus of constructions Dependent type Typed lambda calculus Lambda cube Curry–Howard correspondence Computer Science Applications Pure type system Mathematics
Zdroj:	Mathematical Structures in Computer Science. 9:719-739
ISSN:	1469-8072 0960-1295
Popis:	In this paper we describe a method for proving the normalization property for a large variety of typed lambda calculi of first and second order, which is based on a proof of equivalence of two deduction systems. We first illustrate the method on the elementary example of simply typed lambda calculus, and then we show how to extend it to a more expressive dependent type system. Finally we use it to prove the normalization theorem for Girard's system F.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::62aa1bde1a4b5848e962bcb8951e9872 https://doi.org/10.1017/s0960129599002923 Zobrazit plný text záznamu