Abstract
| Language | English |
|---|---|
| Title of host publication | Programming Languages and Systems |
| Subtitle of host publication | 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings |
| Editors | Hongseok Yang |
| Place of Publication | Cham, Switzerland |
| Publisher | Springer |
| Pages | 56-82 |
| Number of pages | 27 |
| DOIs | |
| State | E-pub ahead of print - 19 Mar 2017 |
| Event | 26th European Symposium on Programming - Uppsala Concert & Congress Hall, Uppsala, Sweden Duration: 22 Apr 2017 → 30 Apr 2017 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 10201 |
| ISSN (Print) | 0302-9743 |
Conference
| Conference | 26th European Symposium on Programming |
|---|---|
| Abbreviated title | ESOP 2017 |
| Country | Sweden |
| City | Uppsala |
| Period | 22/04/17 → 30/04/17 |
Fingerprint
Keywords
- classical linear logic
- communicating processes
- semantics
- cut-elimination rules
Cite this
}
Observed communication semantics for classical processes. / Atkey, Robert.
Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings. ed. / Hongseok Yang. Cham, Switzerland : Springer, 2017. p. 56-82 (Lecture Notes in Computer Science; Vol. 10201).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
TY - GEN
T1 - Observed communication semantics for classical processes
AU - Atkey,Robert
N1 - The final publication is available at link.springer.com
PY - 2017/3/19
Y1 - 2017/3/19
N2 - Classical Linear Logic (CLL) has long inspired readings of its proofs as communicating processes. Wadler's CP calculus is one of these readings. Wadler gave CP an operational semantics by selecting a subset of the cut-elimination rules of CLL to use as reduction rules. This semantics has an appealing close connection to the logic, but does not resolve the status of the other cut-elimination rules, and does not admit an obvious notion of observational equivalence. We propose a new operational semantics for CP based on the idea of observing communication, and use this semantics to define an intuitively reasonable notion of observational equivalence. To reason about observational equivalence, we use the standard relational denotational semantics of CLL. We show that this denotational semantics is adequate for our operational semantics. This allows us to deduce that, for instance, all the cut-elimination rules of CLL are observational equivalences.
AB - Classical Linear Logic (CLL) has long inspired readings of its proofs as communicating processes. Wadler's CP calculus is one of these readings. Wadler gave CP an operational semantics by selecting a subset of the cut-elimination rules of CLL to use as reduction rules. This semantics has an appealing close connection to the logic, but does not resolve the status of the other cut-elimination rules, and does not admit an obvious notion of observational equivalence. We propose a new operational semantics for CP based on the idea of observing communication, and use this semantics to define an intuitively reasonable notion of observational equivalence. To reason about observational equivalence, we use the standard relational denotational semantics of CLL. We show that this denotational semantics is adequate for our operational semantics. This allows us to deduce that, for instance, all the cut-elimination rules of CLL are observational equivalences.
KW - classical linear logic
KW - communicating processes
KW - semantics
KW - cut-elimination rules
UR - http://bentnib.org/cll-obs-semantics.html
UR - http://www.etaps.org/index.php/2017/esop
UR - http://www.springer.com/series/558
U2 - 10.1007/978-3-662-54434-1_3
DO - 10.1007/978-3-662-54434-1_3
M3 - Conference contribution
T3 - Lecture Notes in Computer Science
SP - 56
EP - 82
BT - Programming Languages and Systems
PB - Springer
CY - Cham, Switzerland
ER -