Value-dependent session design in a dependently typed language

De Muijnck-Hughes, Jan and Vanderbauwhede, Wim and Brady, Edwin (2019) Value-dependent session design in a dependently typed language. Electronic Proceedings in Theoretical Computer Science, EPTCS, 291. pp. 47-59. ISSN 2075-2180 (https://doi.org/10.4204/EPTCS.291.5)

[thumbnail of Muijnck-Hughes-etal-EPTCS2019-Value-dependent-session-design-dependently-typed-language]
Preview
 Text. Filename: Muijnck-Hughes-etal-EPTCS2019-Value-dependent-session-design-dependently-typed-language.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (169kB)| Preview

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.

ORCID iDs

De Muijnck-Hughes, Jan ORCID logoORCID: https://orcid.org/0000-0003-2185-8543, Vanderbauwhede, Wim and Brady, Edwin;
  • Item type:Article
    ID code:87355
    Dates:
    Date
    Event
    7 April 2019
    Published
    14 February 2019
    Accepted
    Notes:Publisher Copyright: © Jan de Muijnck-Hughes et al.
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:UNSPECIFIED
    Depositing user: Pure Administrator
    Date deposited:16 Nov 2023 15:52
    Last modified:22 Sep 2024 01:21
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/87355
CORE (COnnecting REpositories)