Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages

Arjen Rouvoet, Casper Poulsen, Robbert Krebbers, Eelco Visser

Research output: Working paper/PreprintWorking paperScientific

83 Downloads (Pure)


An intrinsically-typed definitional interpreter is a concise specification of dynamic semantics, that is executable and type safe by construction. Unfortunately, scaling intrinsically-typed definitional interpreters to more complicated object languages often results in definitions that are cluttered with manual proof work. For linearly-typed languages (including session-typed languages) one has to prove that the interpreter, as well as all the operations on semantic components, treat values linearly. 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. Using these abstractions, we define interpreters for linear lambda calculi with strong references, concurrency, and session-typed communication in Agda
Original languageEnglish
PublisherACM DL
Number of pages15
ISBN (Electronic)978-1-4503-7097-4
Publication statusPublished - 2020


  • Agda
  • Definitional interpreters
  • Dependent types
  • Linear types
  • Mechanized semantics
  • Separation logic
  • Session types
  • Type safety


Dive into the research topics of 'Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages'. Together they form a unique fingerprint.

Cite this