| WoLLIC 2005 Preliminary Version Development Separation in Lambda-Calculus Abstract (2008) | |||||||||||||||
Abstract | |||||||||||||||
| We present a proof technique in λ-calculus that can facilitate inductive reasoning on λ-terms by separating certain β-developments from other β-reductions. We give proofs based on this technique for several fundamental theorems in λ-calculus such as the Church-Rosser theorem, the standardization theorem, the conservation theorem and the normalization theorem. The appealing features of these proofs lie in their inductive styles and perspicuities. Key words: λ-calculus, development, parallel reduction 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||