Time, Location: 14:15, Wednesday 6 December, EM G.61.

Speaker: Jan De Muijnck-Hughes

Title: Type-Driven Development of Communicating Systems using Idris

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.