ST30 2023
who it's for
programming language researchers, session types researchers, formal methods engineers, proof mechanisation engineers, language and runtime implementers, distributed systems engineers
topics
multiparty session type projection; isorecursive session types; computable projection Coq mechanisation; automata-based projection for protocols; benchmarks for message-passing mechanisation; session types for reactive systems; asynchronous and synchronous mixed sessions; session typing for Elixir modules; typestate up and down casting; higher-order to first-order encodings; session-typed consensus; event structures for session types
| title | author | length |
|---|---|---|
| A silent semantics for isorecursive session types | Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos | 30m |
Claim: isorecursive session types can often avoid runtime roll/unroll if all recursions are contractive isorecursive types, and an algorithm extracts adapter… | ||
| Mechanising Multiparty Session Types: A Sound and Complete Projection | Marco Carbone, Dawit Tirore, Jesper Bengtson | 30m |
Defines a new computable projection for multiparty session types and proves it is both sound and complete with respect to the original coinductive counterpart… | ||
| The Concurrent Calculi Formalisation Benchmark | Marco Carbone, David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, Frederik Krogsdal Jacobsen, Alberto Momigliano, Luca Padovani, Alceste Scalas, Martin Vassor, Nobuko Yoshida | 31m |
A new benchmark collection targets machine-checking of message-passing concurrency by giving three concrete problems: mechanize session-type subject reduction… | ||
| Beyond Types for Dyadic Interaction | Nobuko Yoshida | 01h 27m |
Chronicles the 30-year path from Honda’s dyadic session types to multiparty session types and a linear logic correspondence that explains duality and resource… | ||
| Complete Multiparty Session Type Projection with Automata | Elaine Li, Felix Stutz, Thomas Wies, Damien Zufferey | 30m |
Claims a sound, complete, and practical projection operator for asynchronous multiparty session types, implemented by translating global types to automata and… | ||
| Multiparty Reactive Sessions | Ilaria Castellani, Cinzia Di Giusto, Jorge A. Pérez | 29m |
Proposes MRS calculus combining multiparty session types with Synchronous Reactive Programming, adds broadcast, explicit pause/pose for logical instants, and… | ||
| The Expressiveness of Session Types | Jorge A. Pérez | 32m |
Shows that a higher-order session calculus and its first-order fragment are mutually encodable sublanguages with formal correctness proofs, uses a… | ||
| What we learned from writing a book about session types | Simon J. Gay, Vasco T. Vasconcelos | 30m |
A book documents a concrete development path: start from a minimal session calculus with a double-binder design, no primitive data, and mechanized-free proofs… | ||
| So what's the difference between a session type and an ordinary type anyway? | Frank Pfenning | 31m |
Session types differ from ordinary types because they are substructural (linear), they distinguish global vs local specifications, and their channel behavior… | ||
| Behavioural up/down casting for statically typed languages | Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, António Ravara | 23m |
A typestate-based Java tool called JaTyC typestate checker attaches protocols to classes and now supports upcasts and downcasts in the middle of an object’s… | ||
| Session-Based Typechecking for Elixir Modules Using ElixirST | Adrian Francalanza, Gerard Tabone | 32m |
ElixirST provides a static session typing layer for Elixir modules and ships as a compilation‑time tool integrated into the Elixir pipeline. It uses session… | ||
| Asynchronous and Synchronous Mixed Sessions | Kirstin Peters, Nobuko Yoshida | 35m |
Claim: binary session types with mixed choices (CMV+) do not increase synchronous expressiveness — neither for linear nor unrestricted channels — despite… | ||
| Classical Processes in modern dress | Vikraman Choudhury, Simon J. Gay | 37m |
Proposes extending Curry–Howard to a Lambek-style correspondence that ties categorical models of classical linear logic to session-type semantics, and… | ||
| Benchmarks for Multiparty Session Types | Martin Vassor, Nobuko Yoshida | 32m |
Proposal for a community-maintained suite of benchmarks for multiparty session types that collects canonical protocols (two‑buyer, travel agency, etc.)… | ||
| Towards Session-Typed Consensus | Matthew Alan Le Brun, Ornela Dardha | 29m |
Attempts to encode Raft in MAGπ show the calculus models non-Byzantine faults, asynchronous messaging, undirected branching and timeouts but fails to enforce… | ||
| Using Event Structures to model Multiparty Session Types: results and open problems | Ilaria Castellani, Paola Giannini | 37m |
Event Structures are used as a denotational semantics for multiparty session types, producing isomorphic domains of configurations whenever a network is… | ||
| Future Directions for Session Types | Stephanie Balzer, Luís Caires, Ornela Dardha, Raymond Hu | 01h 18m |
Panelists argue concrete next steps: integrate failure handling plus timeouts/congestion into the theory, design a missing module system for session types, and… | ||
| nothing matches | ||