Sciweavers

ENTCS
2006
131views more  ENTCS 2006»
13 years 11 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 thi...
Hongwei Xi