Logo image
Back
A Semantics for Propositions as Sessions
Book chapter   Open access   Peer reviewed

A Semantics for Propositions as Sessions

Sam Lindley and J. Garrett Morris
Programming Languages and Systems, pp.560-584
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2015
DOI: 10.1007/978-3-662-46669-8_23
url
https://doi.org/10.1007/978-3-662-46669-8_23View
Published (Version of record) Open Access

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 deadlock-free, 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.
 Closed Channel Functional Language Linear Logic Reduction Rule Typing Rule

Details

Metrics

36 Record Views
56 Times Cited - Web of Science
Logo image