Separating Sessions Smoothly

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

doi:10.4230/LIPIcs.CONCUR.2021.36

Separating Sessions Smoothly

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	32nd International Conference on Concurrency Theory (CONCUR 2021)
Editors	Serge Haddad, Daniele Varacca
Place of Publication	Dagstuhl, Germany
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages	36:1-36:18
ISBN (Print)	978-3-95977-203-7
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2021.36
Publication status	Published - 13 Aug 2021
Event	32nd International Conference on Concurrency Theory - Online, Paris, France Duration: 23 Aug 2021 → 27 Aug 2021 https://qonfest2021.lacl.fr/concur21.php

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl -- Leibniz-Zentrum für Informatik
Volume	203
ISSN (Electronic)	1868-8969

Conference

Conference	32nd International Conference on Concurrency Theory
Abbreviated title	CONCUR 2021
Country/Territory	France
City	Paris
Period	23/08/21 → 27/08/21
Internet address	https://qonfest2021.lacl.fr/concur21.php

Keywords / Materials (for Non-textual outputs)

session types
hypersequents
linear lambda calculus

Access to Document

10.4230/LIPIcs.CONCUR.2021.36Licence: Creative Commons: Attribution (CC-BY)

Separating Sessions_FOWLER_DOA21062021_VOR_CC-BYFinal published version, 895 KBLicence: Creative Commons: Attribution (CC-BY)

https://drops.dagstuhl.de/opus/volltexte/2021/14413Licence: Creative Commons: Attribution (CC-BY)

2 Finished

Skye-A programming language bridging theory and practice for scientific data curation
Cheney, J. (Principal Investigator)
EU government bodies
1/09/16 → 28/02/23
Project: Research
From Data Types to Session Types - A Basis for Concurrency and Distribution
Wadler, P. (Principal Investigator)
EPSRC
20/05/13 → 19/11/20
Project: Research

1 Article

Separating Sessions Smoothly
Fowler, S., Kokke, W., Dardha, O., Lindley, S. & Morris, J. G., 12 Jul 2023, In: Logical Methods in Computer Science. 19, 3, p. 1-52 52 p.
Research output: Contribution to journal › Article › peer-review

Open Access
File

Cite this

Fowler, S., Kokke, W., Dardha, O., Lindley, S., & Morris, J. G. (2021). Separating Sessions Smoothly. In S. Haddad, & D. Varacca (Eds.), 32nd International Conference on Concurrency Theory (CONCUR 2021) (pp. 36:1-36:18). (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 203). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2021.36

@inproceedings{b890e2502b0643548713e9fc0b5f620b,

title = "Separating Sessions Smoothly",

abstract = "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{\textquoteright}s Mix rule, a crucial ingredient for channel forwarding and exceptions.",

keywords = "session types, hypersequents, linear lambda calculus",

author = "Simon Fowler and Wen Kokke and Ornela Dardha and Sam Lindley and Morris, \{J. Garrett\}",

year = "2021",

month = aug,

day = "13",

doi = "10.4230/LIPIcs.CONCUR.2021.36",

language = "English",

isbn = "978-3-95977-203-7",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

pages = "36:1--36:18",

editor = "Serge Haddad and Daniele Varacca",

booktitle = "32nd International Conference on Concurrency Theory (CONCUR 2021)",

note = "32nd International Conference on Concurrency Theory, CONCUR 2021 ; Conference date: 23-08-2021 Through 27-08-2021",

url = "https://qonfest2021.lacl.fr/concur21.php",

}

Fowler, S, Kokke, W, Dardha, O, Lindley, S & Morris, JG 2021, Separating Sessions Smoothly. in S Haddad & D Varacca (eds), 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 203, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 36:1-36:18, 32nd International Conference on Concurrency Theory, Paris, France, 23/08/21. https://doi.org/10.4230/LIPIcs.CONCUR.2021.36

Separating Sessions Smoothly. / Fowler, Simon; Kokke, Wen; Dardha, Ornela et al.
32nd International Conference on Concurrency Theory (CONCUR 2021). ed. / Serge Haddad; Daniele Varacca. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. p. 36:1-36:18 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 203).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Separating Sessions Smoothly

AU - Fowler, Simon

AU - Kokke, Wen

AU - Dardha, Ornela

AU - Lindley, Sam

AU - Morris, J. Garrett

PY - 2021/8/13

Y1 - 2021/8/13

N2 - 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.

AB - 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.

KW - session types

KW - hypersequents

KW - linear lambda calculus

U2 - 10.4230/LIPIcs.CONCUR.2021.36

DO - 10.4230/LIPIcs.CONCUR.2021.36

M3 - Conference contribution

SN - 978-3-95977-203-7

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 36:1-36:18

BT - 32nd International Conference on Concurrency Theory (CONCUR 2021)

A2 - Haddad, Serge

A2 - Varacca, Daniele

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

CY - Dagstuhl, Germany

T2 - 32nd International Conference on Concurrency Theory

Y2 - 23 August 2021 through 27 August 2021

ER -

Separating Sessions Smoothly

Abstract

Publication series

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

Skye-A programming language bridging theory and practice for scientific data curation

From Data Types to Session Types - A Basis for Concurrency and Distribution

Research output

Separating Sessions Smoothly

Cite this