Since 2014
Names, Equations, Relations: Practical Ways to Reason about new
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Names, Equations, Relations: Practical Ways to Reason about new
|
|
| Creator |
Stark, Ian
|
|
| Description |
The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with statein the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction betweennames and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculushas 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 toreason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs ofcontextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power butin a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.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 ThirdInternational Conference TLCA '97, Lecture Notes in Computer Science 1210, Springer-Verlag 1997. |
|
| Publisher |
Aarhus University
|
|
| Date |
1997-06-09
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18965
10.7146/brics.v4i39.18965 |
|
| Source |
BRICS Report Series; No 39 (1997): RS-39 Names, Equations, Relations: Practical Ways to Reason about new
BRICS Report Series; Nr. 39 (1997): RS-39 Names, Equations, Relations: Practical Ways to Reason about new 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18965/16604
|
|