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

Ian Stark*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 other kinds of local declaration, and to the mobile processes of the π-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.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications: Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Nancy, France, April 2–4, 1997
EditorsPhilippe de Groote, J. Roger Hindley
PublisherSpringer
Pages336-353
Number of pages18
ISBN (Print)3540626883, 9783540626886
DOIs
Publication statusPublished - 1997
Event3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997 - Nancy, France
Duration: 2 Apr 19974 Apr 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1210
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997
Country/TerritoryFrance
CityNancy
Period2/04/974/04/97

Fingerprint

Dive into the research topics of 'Names, Equations, Relations: Practical Ways to Reason about new'. Together they form a unique fingerprint.

Cite this