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

Session types are a rich type discipline, based on linear types, that
lift the sort of safety claims that come with type systems to
communications. However, web-based applications and micro services
are often written in a mix of languages, with type disciplines in a
spectrum between static and dynamic typing. Gradual session types
address this mixed setting by providing a framework which grants
seamless transition between statically typed handling of sessions and
any required degree of dynamic typing.

We propose GradualGV as an extension of the functional session type
system GV with dynamic types and casts. We demonstrate type and
communication safety as well as blame safety, thus extending previous
results to functional languages with session-based communication. The
interplay of linearity and dynamic types requires a novel approach to
specifying the dynamics of the language.

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
22m
Talk
Chaperone Contracts for Higher-Order Sessions
Research Papers
Hernan MelgrattiUniversity of Buenos Aires, Argentina, Luca PadovaniUniversity of Turin, Italy
DOI
13:22
22m
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
22m
Talk
Manifest Sharing with Session Types
Research Papers
Stephanie BalzerCarnegie Mellon University, USA, Frank PfenningCarnegie Mellon University, USA
DOI
14:07
22m
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