A semantics for propositions as sessions

Sam Lindley, J. Garrett Morris

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

36 Citations (Scopus)

Abstract

Session types provide a static guarantee that concurrent programs respect communication protocols. Recently, Caires, Pfenning, and Toninho, and Wadler, have developed a correspondence between propositions of linear logic and session typed π-calculus processes. We relate the cut-elimination semantics of this approach to an operational semantics for session-typed concurrency in a functional language. We begin by presenting a variant of Wadler’s session-typed core functional language, GV. We give a small-step operational semantics for GV.We develop a suitable notion of deadlock, based on existing approaches for capturing deadlock in π-calculus, and show that all well-typed GV programs are deadlockfree, deterministic, and terminating. We relate GV to linear logic by giving translations between GV and CP, a process calculus with a type system and semantics based on classical linear logic. We prove that both directions of our translation preserve reduction; previous translations from GV to CP, in contrast, failed to preserve β-reduction. Furthermore, to demonstrate the modularity of our approach, we define two extensions of GV which preserve deadlock-freedom, determinism, and termination.

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publicationESOP 2015
EditorsJan Vitek
PublisherSpringer
Pages560-584
Number of pages25
ISBN (Electronic)9783662466698
ISBN (Print)9783662466681
DOIs
Publication statusPublished - 2015
Event24th European Symposium on Programming 2015 - London, United Kingdom
Duration: 11 Apr 201518 Apr 2015

Publication series

NameLecture Notes in Computer Science
Volume9032
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th European Symposium on Programming 2015
Abbreviated titleESOP 2015
CountryUnited Kingdom
CityLondon
Period11/04/1518/04/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A semantics for propositions as sessions'. Together they form a unique fingerprint.

  • Profiles

    Cite this

    Lindley, S., & Garrett Morris, J. (2015). A semantics for propositions as sessions. In J. Vitek (Ed.), Programming Languages and Systems: ESOP 2015 (pp. 560-584). (Lecture Notes in Computer Science; Vol. 9032). Springer. https://doi.org/10.1007/978-3-662-46669-8_23