Development Separation in Lambda-Calculus

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

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Hongwei Xi
• Keywords: Certain -developments, ENTCS 2006, Inductive Reasoning, Proof Technique