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.