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

Contracts have proved to be an effective mechanism that helps developers in identifying those modules of a program that violate the contracts of the functions and objects they use. In recent years, sessions have established as a key mechanism for realizing inter-module communications in concurrent programs. Just like values flow into or out of a function or object, messages are sent on, and received from, a session endpoint. Unlike conventional functions and objects, however, the kind, direction, and properties of messages exchanged in a session may vary over time, as the session progresses. This feature of sessions calls for contracts that evolve along with the session they describe.

In this work, we extend to sessions the notion of chaperone contract (roughly, a contract that applies to a mutable object) and investigate the ramifications of contract monitoring in a higher-order language that features sessions. We give a characterization of correct module, one that honors the contracts of the sessions it uses, and prove a blame theorem. Guided by the calculus, we describe a lightweight implementation of monitored sessions as an OCaml module with which programmers can benefit from static session type checking and dynamic contract monitoring using an off-the-shelf version of OCaml.

Wed 6 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change

13:00 - 14:30: Contracts and SessionsResearch Papers at L1
Chair(s): Matthew FlattUniversity of Utah
13:00 - 13:22
Talk
Chaperone Contracts for Higher-Order Sessions
Research Papers
Hernan MelgrattiUniversity of Buenos Aires, Argentina, Luca PadovaniUniversity of Turin, Italy
DOI
13:22 - 13:45
Talk
Whip: Higher-Order Contracts for Modern Services
Research Papers
Lucas WayeHarvard University, USA, Christos DimoulasHarvard University, USA, Stephen ChongHarvard University, USA
DOI
13:45 - 14:07
Talk
Manifest Sharing with Session Types
Research Papers
Stephanie BalzerCarnegie Mellon University, USA, Frank PfenningCarnegie Mellon University, USA
DOI
14:07 - 14:30
Talk
Gradual Session Types
Research Papers
Atsushi IgarashiKyoto University, Japan, Peter ThiemannUniversity of Freiburg, Germany, Vasco VasconcelosUniversity of Lisbon, Portugal, Philip WadlerUniversity of Edinburgh, UK
DOI