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

Fundamenta
Informaticae, 33(4):369-396, April 1998.

This article is the complete version of a paper
presented at TLCA '97. A preliminary version appeared as BRICS Report RS-97-39 in December 1997.

Fetch article (PDF, 222k). Go to publications, talks or home page.

### Abstract

The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with
state in the form of dynamically-generated *names*. These names can
be created locally, passed around, and compared with one another. Through
the interaction between names and functions, the language can capture
notions of scope, visibility and sharing. Originally motivated by the study
of references in Standard ML, the nu-calculus has connections to local
declarations in general; to the mobile processes of the pi-calculus; and to
security protocols in the spi-calculus.

This paper introduces a logic of equations and relations which allows one to
reason about expressions of the nu-calculus: this uses a simple
representation of the private and public scope of names, and allows
straightforward proofs of contextual equivalence (also known as
observational, or observable, equivalence). 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.

@Article{stark:namerp-fi,
author = {Ian Stark},
title = {Names, Equations, Relations:
Practical Ways to Reason about {\em new}},
journal = {Fundamenta Informaticae},
year = 1998,
month = {April},
volume = 33,
number = 4,
pages = {369--396},
note = {Complete version of \cite{stark:namerp-tlca}},
url = {http://www.inf.ed.ac.uk/~stark/namerp-fi.html}
}

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