Write a Blog >>
Tue 21 Jan 2020 14:43 - 15:05 at Maurepas - Concurrency and linearity Chair(s): Zhong Shao

An intrinsically-typed definitional interpreter is an attractive way of specifying the dynamic semantics of a programming language. It is a concise specification that is executable and type safe by construction. Unfortunately, scaling up intrinsically-typed definitional interpreters to more complicated object languages often results in definitions that are cluttered with manual proof work. In linearly-typed languages (e.g., session-typed languages) one has to ensure that all values are used linearly, and that linearity is maintained throughout the definition of the interpreter.

We present new methods and tools that make it possible to implement intrinsically-typed definitional interpreters for linearly-typed languages in a way that hides the majority of the manual proof work. Inspired by separation logic, we develop reusable and composable abstractions for programming with linear operations using dependent types. We use these abstractions to define interpreters for linearly-typed lambda calculi with strong references, and concurrent, session-typed communication in Agda.

Slides (neworleans.pdf)134KiB

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

14:00 - 15:05: Concurrency and linearityCPP at Maurepas
Chair(s): Zhong ShaoYale University
14:00 - 14:21
Formalizing Determinacy of Concurrent Revisions
Roy OverbeekVrije Universiteit Amsterdam
DOI Pre-print Media Attached
14:21 - 14:43
Formalizing π-calculus in Guarded Cubical Agda
Niccolò VeltriTallinn University of Technology, Andrea VezzosiIT University Copenhagen
DOI Pre-print Media Attached File Attached
14:43 - 15:05
Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Arjen RouvoetDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology
DOI Pre-print Media Attached File Attached