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

Arjen Rouvoet, Casper Poulsen, Robbert Krebbers, Eelco Visser

Research output: Working paper/PreprintWorking paperScientific

64 Downloads (Pure)

Abstract

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
Pages284-298
Number of pages15
ISBN (Electronic)978-1-4503-7097-4
DOIs
Publication statusPublished - 2020

Keywords

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

Fingerprint

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

Cite this