| Generalized λ-Calculi (Abstract) (2007) | |||||||||||||||
Abstract | |||||||||||||||
| ) Hongwei Xi Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, PA 15213, USA email: hwxi@cs.cmu.edu Fax: +1 412 268 6380 We propose a notion of generalized -calculi, which include the usual call-by-name -calculus, the usual call-by-value -calculus, and many other -calculi such as the g -calculus[3], the v hd -calculus[5], etc. We prove the Church-Rosser theorem and the standardization theorem for these generalized -calculi. The normalization theorem then follows, which enables us to define evaluation functions for the generalized -calculi. Our proof technique mainly establishes on the notion of separating developments[4], yielding intuitive and clean inductive proofs. This work aims at providing a solid foundation for evaluation under -abstraction, a notion which is pervasive in both partial evaluation and run-time code generation for functional programming languages. Definition1. We use the following for -terms and contexts: (terms) L; M;N ::= x j ... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||