A Functional Theory of Local Names

Martin Odersky

Revised from a paper presented at the 21st ACM Symposium on
Principles of Programming Languages, January 1994, pp 48-58.

$\lambda\nu$ is an extension of the $\lambda$-calculus with a binding
construct for local names. The extension has properties analogous to
classical $\lambda$-calculus and preserves all observational
equivalences of $\lambda$. It is useful as a basis for modeling
wide-spectrum languages that build on a functional core.