Skip to content

Research at St Andrews

Value-dependent session design in a dependently typed language

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Jan de Muijnck-Hughes, Edwin Charles Brady, Wim Vanderbauwhede

School/Research organisations

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.
Close

Details

Original languageEnglish
Title of host publicationProceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, Prague, Czech Republic, 7th April 2019
EditorsFrancisco Martins, Dominic Orchard
PublisherOpen Publishing Association
Pages47-59
DOIs
Publication statusPublished - 2 Apr 2019
EventProgramming Language Approaches to Concurrency- & Communication-cEntric Software (PLACES 2019)
- Prague, Czech Republic
Duration: 7 Apr 20197 Apr 2019
Conference number: 11
https://conf.researchr.org/track/etaps-2019/places-2019-papers

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume291
ISSN (Electronic)2075-2180

Workshop

WorkshopProgramming Language Approaches to Concurrency- & Communication-cEntric Software (PLACES 2019)
Abbreviated titlePLACES
CountryCzech Republic
CityPrague
Period7/04/197/04/19
Internet address

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Subtype polymorphism à la carte via machine learning on dependent types

    Swan, J., Johnson, C. G. & Brady, E. C., 16 Jul 2018, Companion Proceedings for the ISSTA/ECOOP 2018 Workshops. New York, NY: Association for Computing Machinery, Inc, p. 14-16 3 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Type driven development of concurrent communicating systems

    Brady, E. C., 7 Jul 2017, In : Computer Science. 18, 3, 22 p., 1413.

    Research output: Contribution to journalArticle

  3. Sequential decision problems, dependent types and generic solutions

    Botta, N., Jansson, P., Ionescu, C., Christiansen, D. & Brady, E. C., 17 Mar 2017, In : Logical Methods in Computer Science. 13, 1, 23 p., 7.

    Research output: Contribution to journalArticle

  4. Type-driven development with Idris

    Brady, E. C., Mar 2017, Shelter Island: Manning Publications Co. 480 p.

    Research output: Book/ReportBook

  5. Automatically proving equivalence by type-safe reflection

    Slama, F. & Brady, E. C., 2017, Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 40-55 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 258172592

Top