Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
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.
Conference DayTue 21 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
|Formalizing Determinacy of Concurrent Revisions|
Roy OverbeekVrije Universiteit AmsterdamDOI Pre-print Media Attached
|Formalizing π-calculus in Guarded Cubical Agda|
CPPDOI Pre-print Media Attached File Attached
|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 TechnologyDOI Pre-print Media Attached File Attached