Value-dependent session design in a dependently typed language

Jan De Muijnck-Hughes, Wim Vanderbauwhede, Edwin Brady

Research output: Contribution to journalConference articlepeer-review

7 Citations (Scopus)
11 Downloads (Pure)

Abstract

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.

Original languageEnglish
Pages (from-to)47-59
Number of pages13
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume291
DOIs
Publication statusPublished - 7 Apr 2019
Event11th Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2019 - Prague, Czech Republic
Duration: 7 Apr 20197 Apr 2019

Keywords

  • session types
  • type-checking
  • dependently typed language
  • Idris
  • arithmetic operations
  • protocol specifications
  • protocol description
  • TCP handshake

Fingerprint

Dive into the research topics of 'Value-dependent session design in a dependently typed language'. Together they form a unique fingerprint.

Cite this