Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the from 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 declaations in general; to the mobile processes of the p-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 based on earlier operational techniques, providing the same power but in a much more accessible from. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.
Wydawca
Czasopismo
Rocznik
Tom
Strony
369--396
Opis fizyczny
bibliogr. 38 poz.
Twórcy
autor
- Department of Computer Science The University of Edinburgh Scotland, Ian.Stark@ed.ac.uk
Bibliografia
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS1-0003-0034