Observed communication semantics for classical processes

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

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.
LanguageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication26th 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
EditorsHongseok Yang
Place of PublicationCham, Switzerland
PublisherSpringer
Pages56-82
Number of pages27
DOIs
StateE-pub ahead of print - 19 Mar 2017
Event26th European Symposium on Programming - Uppsala Concert & Congress Hall, Uppsala, Sweden
Duration: 22 Apr 201730 Apr 2017

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10201
ISSN (Print)0302-9743

Conference

Conference26th European Symposium on Programming
Abbreviated titleESOP 2017
CountrySweden
CityUppsala
Period22/04/1730/04/17

Fingerprint

Semantics
Communication

Keywords

  • classical linear logic
  • communicating processes
  • semantics
  • cut-elimination rules

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). Cham, Switzerland: Springer. DOI: 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",
year = "2017",
month = "3",
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. DOI: 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 proceedingConference 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 -

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). Available from, DOI: 10.1007/978-3-662-54434-1_3