David, René A simple proof of basic results in \(\lambda\) calculus. (Une preuve simple de résultats classiques en \(\lambda\) calcul.) (French. Abridged English version) Zbl 0830.03003 C. R. Acad. Sci., Paris, Sér. I 320, No. 11, 1401-1406 (1995). Summary: We give a simple proof of three basic theorems of pure lambda calculus: the Church-Rosser theorem, the standardisation theorem and the finiteness of developments theorem. We also give an extension – in pure calculus – of the latter that immediately gives the strong normalisation theorem for the type system \(D\) (simple types with intersection). Cited in 5 Documents MSC: 03B40 Combinatory logic and lambda calculus Keywords:lambda calculus; Church-Rosser theorem; standardisation theorem; finiteness of developments theorem; strong normalisation theorem PDFBibTeX XMLCite \textit{R. David}, C. R. Acad. Sci., Paris, Sér. I 320, No. 11, 1401--1406 (1995; Zbl 0830.03003)