Speaker: Jan de Muijnck-Hughes

Abstract

Communicating protocols are a cornerstone of modern system design.
However, there is a disconnect between the different tooling used to design, implement and reason about these protocols and their implementations.
Session Types are a typing discipline that help resolve this difference by allowing protocol specifications to be used during type-checking to ensure that implementations adhere to a given specification.

Idris is a general purpose programming language that supports full-dependent types, providing programmers with the ability to reason more precisely about programs.
This talk introduces =Sessions=, our implementation of Session Types in Idris, and demonstrates =Sessions= ability to design and realise several common protocols.

=Sessions= improves upon existing Session Type implementations by introducing value dependencies between messages and fine-grained channel management during protocol design and implementation.
We also use Idris’ support for EDSL construction to allow for protocols to be designed and reasoned about in the same language as their implementation.
Thereby allowing for an intrinsic bond to be introduced between a protocol’s implementation and specification, and also with its verification.

Using =Sessions=, we can reduce the existing disconnect between the tooling used for protocol design, implementation, and verification.