Duality of Session Types: The Final Cut

Simon J. Gay
(School of Computing Science, University of Glasgow, UK)
Peter Thiemann
(Institut für Informatik, University of Freiburg, Germany)
Vasco T. Vasconcelos
(Faculdade de Ciências, University of Lisbon, Portugal)

Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda.

In Stephanie Balzer and Luca Padovani: Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2020), Dublin, Ireland, 26th April 2020, Electronic Proceedings in Theoretical Computer Science 314, pp. 23–33.
Published: 3rd April 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.314.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org