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.

Tue 21 Jan

CPP-2020-papers
14:00 - 15:05: CPP 2020 - Concurrency and linearity at Maurepas
Chair(s): Zhong ShaoYale University
CPP-2020-papers14:00 - 14:21
Talk
Roy OverbeekVrije Universiteit Amsterdam
Pre-print
CPP-2020-papers14:21 - 14:43
Talk
Niccolò VeltriTallinn University of Technology, Andrea VezzosiIT University Copenhagen
Pre-print
CPP-2020-papers14:43 - 15:05
Talk
Arjen RouvoetDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology
Pre-print