Sam Lindley

Embedding session types in Haskell

2016

We present a novel embedding of session-typed concurrency in Haskell. We extend an existing HOAS embedding of linear λ-calculus with a set of core session-typed primitives, using indexed type families to express the constraints of …

Separating Sessions Smoothly

2021 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

<p>This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, …