<p>The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state<br />in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between<br />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<br />has connections to local declarations in general; to the mobile processes of the pi-calculus; and to security protocols in the spi-calculus. <br /> This paper introduces a logic of equations and relations which allows one to<br />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<br />contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but<br />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.</p><p>This supersedes the earlier BRICS Report RS-96-31. It also expands on the paper presented in Typed Lambda Calculi and Applications: Proceedings of the Third<br />International Conference TLCA '97, Lecture Notes in Computer Science 1210, Springer-Verlag 1997.</p>
A New Proof of P-time Completeness of Linear Lambda Calculus
