In Typed Lambda Calculi and Applications: Proceedings of the Third International Conference TLCA '97, Nancy, France, April 2-4, 1997. Lecture Notes in Computer Science 1210, pages 336-353. Springer-Verlag, 1997.
The full version of this paper appears as an article in Fundamenta Informaticae, April 1998.
Fetch paper (PDF, 201k) or conference slides (PDF, 47k). Go to publications, talks or home page.
Many convenient features of programming languages today involve some notion of `names': anonymous tags that can be taken on demand from some infinite supply. Names are quite independent of programming style or flow-of-control issues; they arise in languages for imperative, functional or concurrent computation, and are useful in discussing distribution, mobility and security of code. Examples range from Lisp's `gensym' to the dynamically created channels of the pi-calculus.
The nu-calculus was devised to explore the abstract behaviour of names, by adding them to a simply-typed lambda-calculus. It turns out that the interaction with higher-order functions exposes many of the delicate aspects of names: unguessability, privacy, flexible scope, persistence, anonymity, ... . The nu-calculus is then a good place to start reasoning about the behaviour of names.
This paper introduces a logic of equations and relations for proving properties of the nu-calculus. Through a simple representation of `private' and `public' it allows direct calculation of equivalences between expressions that use names. The logic is based on earlier operational techniques, providing the same power but in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.
@InProceedings{stark:namerp-tlca,
author = {Ian Stark},
title = {Names, Equations, Relations: Practical
Ways to Reason about {\em new}},
booktitle = {Typed Lambda Calculi and Applications:
Proceedings of the Third International
Conference TLCA~'97},
series = {Lecture Notes in Computer Science},
number = 1210,
pages = {336--353},
publisher = {Springer-Verlag},
year = 1997,
note = {A full version appears as \cite{stark:namerp-fi}},
url = {http://www.inf.ed.ac.uk/~stark/namerp-tlca.html}
}