Observed communication semantics for classical processes

Robert Atkey

doi:10.1007/978-3-662-54434-1_3

Observed communication semantics for classical processes

Robert Atkey

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

11 Citations (Scopus)

47 Downloads (Pure)

Abstract

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.

Original 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	https://doi.org/10.1007/978-3-662-54434-1_3
Publication status	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/Territory	Sweden
City	Uppsala
Period	22/04/17 → 30/04/17

Keywords

classical linear logic
communicating processes
semantics
cut-elimination rules

Access to Document

10.1007/978-3-662-54434-1_3

Atkey-ESOP2017-Observed-communication-semantics-for-classical-processesAccepted author manuscript, 426 KB

Cite this

Atkey, R. (2017). Observed communication semantics for classical processes. In H. Yang (Ed.), 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 (pp. 56-82). (Lecture Notes in Computer Science; Vol. 10201). Springer. https://doi.org/10.1007/978-3-662-54434-1_3

Atkey, Robert. / Observed communication semantics for classical processes. 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. editor / Hongseok Yang. Cham, Switzerland : Springer, 2017. pp. 56-82 (Lecture Notes in Computer Science).

@inproceedings{2a7e38f7505f404f9be67ef3d3191cd9,

title = "Observed communication semantics for classical processes",

abstract = "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.",

keywords = "classical linear logic, communicating processes, semantics, cut-elimination rules",

author = "Robert Atkey",

note = "The final publication is available at link.springer.com; 26th European Symposium on Programming, ESOP 2017 ; Conference date: 22-04-2017 Through 30-04-2017",

year = "2017",

month = mar,

day = "19",

doi = "10.1007/978-3-662-54434-1_3",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "56--82",

editor = "Hongseok Yang",

booktitle = "Programming Languages and Systems",

}

Atkey, R 2017, Observed communication semantics for classical processes. in H Yang (ed.), 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. Lecture Notes in Computer Science, vol. 10201, Springer, Cham, Switzerland, pp. 56-82, 26th European Symposium on Programming, Uppsala, Sweden, 22/04/17. https://doi.org/10.1007/978-3-662-54434-1_3

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 book

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 book

T3 - Lecture Notes in Computer Science

SP - 56

EP - 82

BT - Programming Languages and Systems

A2 - Yang, Hongseok

PB - Springer

CY - Cham, Switzerland

T2 - 26th European Symposium on Programming

Y2 - 22 April 2017 through 30 April 2017

ER -

Atkey R. Observed communication semantics for classical processes. In Yang H, editor, 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. Cham, Switzerland: Springer. 2017. p. 56-82. (Lecture Notes in Computer Science). Epub 2017 Mar 19. doi: 10.1007/978-3-662-54434-1_3

Observed communication semantics for classical processes

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint