Posted on March 7, 2019
Categories: idris, dependent-types, session-types, paper, places, tdvcs, glasgow
The Glasgow site are very pleased to announce that Jan’s paper on designing a global session description language within Idris was accepted to PLACES 2019. This was an extension of ideas that he and [Edwin Brady]{https://www.cs.st-andrews.ac.uk/directory/person?id=eb} had as part of the TDVCS project, that were then matured in the Border Patrol project with Wim Vanderbauwhede.
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.
More details will follow the workshop itself, and once DOIs have been minted.