This week, I gave a talk about my work with Edwin Brady at University of St Andrews, whilst visiting Imperial College London for the Border Patrol Project. The talk was an extended version of my FP-Dag Talk, which was a revamp of my SPLS talk.
There is a disconnect between the tooling used to design, implement and reason about communication 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.
This talk introduces
Sessions, an adaptation of Session Types in Idris, and demonstratesSessionsability to design and realise several common protocols. Limitations will be discussed as well. Idris is a general purpose programming language that supports full-spectrum dependent types, providing programmers with the ability to reason more precisely about programs.
Sessionsimproves 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 protocol design and analysis to occur 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.
Slides are not available online.