A Syntactic Theory of Local Names
Martin Odersky
Research Report YALEU/DCS/RR-965
Department of Computer Science, Yale University
May 1993
Lambda-nu is an extension of the Lambda-calculus with a binding
construct for local names. The extension is symmetric in identifiers
and names, it has properties analogous to classical
Lambda-calculus, and it preserves all observational equivalences of
Lambda. The calculus is useful as a basis for modeling
wide-spectrum languages that build on a functional core.