SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Mon 23 Oct 2023 12:00 - 12:30 at Room XIII - ST30 Day 2 Session 2 Chair(s): Frank Pfenning

The computational interpretation of linear logic as a session-typed pi calculus has motivated many developments, and can be accepted as a fairly canonical typed model for stateful concurrent computation with linear resources, pretty much like the lambda calculus is considered a canonical typed model for functional sequential computation with pure values. Building on this logical approach, in this talk we will discuss labelled tensor session types, namely record and mutable record types and their duals, which substantially increase the flexibility in linearly-typed session-based programming. Labelled tensor types support random access paths to ``data-structures-as-processes" and relaxing acyclicity constraints from trees to dags in shared linear data structures. We will also offer further motivation, formally present labelled tensor types, their typing rules and metatheory, compare with recent work on linear type systems for concurrent and message passing programming and demonstrate their expressiveness in realistic concurrent session-based shared-state programs written in an extension of our CLASS implementation.

Mon 23 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
ST30 Day 2 Session 2ST30 at Room XIII
Chair(s): Frank Pfenning Carnegie Mellon University, USA
11:00
30m
Talk
Asynchronous and Synchronous Mixed Sessions
ST30
Kirstin Peters Augsburg University, Nobuko Yoshida University of Oxford
11:30
30m
Talk
Classical Processes in modern dress
ST30
Vikraman Choudhury University of Glasgow, Simon J. Gay University of Glasgow, UK
12:00
30m
Talk
Labelled Tensor Types in Session Based ProgrammingCancelled
ST30
Luís Caires INESC-ID / Instituto Superior Tecnico, University of Lisbon