## Names, Equations, Relations: Practical Ways to Reason about
*new*

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.

### Abstract

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}
}

#### Page last modified:
Tuesday 5 August 2008