Sciweavers

ENTCS
2006

Development Separation in Lambda-Calculus

13 years 9 months ago
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
Hongwei Xi
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Hongwei Xi
Comments (0)