Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Wed 6 Sep 2017 13:45 - 14:07 at L1 - Contracts and Sessions Chair(s): Matthew Flatt

Session-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared resources. In this paper, we introduce sharing into a session-typed language where types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. We illustrate our language on various examples, such as the dining philosophers problem, and provide a translation of the untyped asynchronous $\pi$-calculus into our language.

Wed 6 Sep

Displayed time zone: Belfast change

13:00 - 14:30
Contracts and SessionsResearch Papers at L1
Chair(s): Matthew Flatt University of Utah
13:00
22m
Talk
Chaperone Contracts for Higher-Order Sessions
Research Papers
Hernan Melgratti University of Buenos Aires, Argentina, Luca Padovani University of Turin, Italy
DOI
13:22
22m
Talk
Whip: Higher-Order Contracts for Modern Services
Research Papers
Lucas Waye Harvard University, USA, Christos Dimoulas Harvard University, USA, Stephen Chong Harvard University, USA
DOI
13:45
22m
Talk
Manifest Sharing with Session Types
Research Papers
Stephanie Balzer Carnegie Mellon University, USA, Frank Pfenning Carnegie Mellon University, USA
DOI
14:07
22m
Talk
Gradual Session Types
Research Papers
Atsushi Igarashi Kyoto University, Japan, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos University of Lisbon, Portugal, Philip Wadler University of Edinburgh, UK
DOI