• Jan De Muijnck-Hughes – Type-Driven Development of Communicating Systems using Idris (6th December, 2017)

    by  • December 1, 2017 • DSG Research Seminars: Logic and Programming Languages

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

    Speaker: Jan De Muijnck-Hughes

    Title: Type-Driven Development of Communicating Systems using Idris


    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

    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.