Invited Talk: Gradual Session Types — an Ongoing Journey
Gradual Session Types enable the connection of typed and untyped clients of a protocol. The type checker guarantees that the typed client follows the protocol, whereas dynamic checks, generated by gradual session type inference, guarantee that the untyped client follows the protocol, too. The journey begins with a coercion calculus that extends Gay and Vasconcelos functional session type language and considers a surface language and gradual type inference. It continues with the observation that the untyped language is not sufficiently untyped and offers a more economic calculus as a basis for a surface language that supports untyped programming in a satisfactory style.
Parts of this work are based on collaboration with Atsushi Igarashi, Vasco Vasconcelos, and Phil Wadler.
Sun 13 Jan
|08:30 - 08:40|
|08:40 - 09:30|
Peter ThiemannUniversity of Freiburg, Germany
|09:30 - 09:50|
|09:50 - 10:10|
Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco VasconcelosLASIGE, Faculty of Sciences, University of LisbonFile Attached
|10:10 - 10:30|
Alceste ScalasImperial College London, Elias BenussiImperial College London, Nobuko YoshidaImperial College LondonFile Attached