Separating Sessions Smoothly

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, J. Garrett Morris

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard’s Mix rule, a crucial ingredient for channel forwarding and exceptions.
Original languageEnglish
Title of host publication32nd International Conference on Concurrency Theory (CONCUR 2021)
EditorsSerge Haddad, Daniele Varacca
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
ISBN (Print)978-3-95977-203-7
Publication statusPublished - 13 Aug 2021
Event32nd International Conference on Concurrency Theory - Online, Paris, France
Duration: 23 Aug 202127 Aug 2021

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl -- Leibniz-Zentrum für Informatik
ISSN (Electronic)1868-8969


Conference32nd International Conference on Concurrency Theory
Abbreviated titleCONCUR 2021
Internet address


  • session types
  • hypersequents
  • linear lambda calculus


Dive into the research topics of 'Separating Sessions Smoothly'. Together they form a unique fingerprint.

Cite this