Posted on February 5, 2019
Categories: idris, hardware, substructural-type-systems, session-types, dependent-types, glasgow, plug, tdd
Jan gave an internal seminar at PLUG in which he discussed work on implementing global session descriptions as an EDSL within Idris.
The abstract is:
Communication protocols are a cornerstone of modern system design. However, there is a disconnect between the tooling used to design, implement and reason about these protocols and their implementations. Session Types offer a typing discipline that helps resolve this difference by allowing protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. Session Type implementations are, however, limited in their expressiveness in protocol design and implementation.
In previous (unpublished) joint work with Edwin Brady, we investigated how to realise a Multi-Party Session-Types inspired language within the dependently typed language Idris. Our work allowed rich protocol descriptions to be described in, and intrinsicly linked, to the protocol implementation: communicating systems were correct-by-construction. A major limitation of our work was that we could not reason competently about value-dependent messages. These are messages that rely upon values previously seen in the protocol.
Recently, I have had a chance to revisit this work and found a interesting solution using /Resource Dependent EDSLs/ to describe value dependent session descriptions. In this talk I will describe the underlying construction techniques employed; demonstrate the ability of our new session description language to describe interesting protocols; and discuss future directions and re-visitations of my previous work.
Slides are not available.