Labelled Tensor Types in Session Based ProgrammingCancelled
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 OctDisplayed time zone: Lisbon change
11:00 - 12:30 | |||
11:00 30mTalk | Asynchronous and Synchronous Mixed Sessions ST30 | ||
11:30 30mTalk | Classical Processes in modern dress ST30 | ||
12:00 30mTalk | Labelled Tensor Types in Session Based ProgrammingCancelled ST30 Luís Caires INESC-ID / Instituto Superior Tecnico, University of Lisbon |