ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sun 7 Apr 2019 16:00 - 16:30 at S8 - IV Chair(s): Francisco Martins

Session Types offer a typing discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care must be taken that values introduced in the description are used by roles that know about the value.

We present Sessions, a Resource Dependent Embedded Domain Specific Language (EDSL) for describing global session descriptions in the dependently typed language Idris. As we construct session descriptions the values parameterising the EDSLs’ type keeps track of roles and messages they have encountered. We can use this knowledge to ensure that message values are only used by those who know the value. Sessions supports protocol descriptions that are computable, composable, higher-order, and value-dependent. We demonstrate Sessions expressiveness by describing the TCP Handshake, a multi-modal server providing echo and basic arithmetic operations, and a Higher-Order protocol that supports an authentication interaction step.

Sun 7 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:00: IVPLACES at S8
Chair(s): Francisco MartinsUniversity of Lisbon
16:00 - 16:30
Value-Dependent Session Design in a Dependently Typed Language
Jan de Muijnck-HughesUniversity of Glasgow, Edwin BradyUniversity of St. Andrews, UK, Wim VanderbauwhedeUniversity of Glasgow
16:30 - 17:00
Fluid Types: Statically Verified Distributed Protocols with Refinements
Fangyi ZhouImperial College London, Francisco FerreiraImperial College London, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London
17:00 - 17:30
The Cpi-calculus: a Model for Confidential Name Passing
Ivan ProkićUniversity of Novi Sad
17:30 - 17:35
Day closing
Closing remarks