TY - UNPB
T1 - Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
AU - Rouvoet, Arjen
AU - Poulsen, Casper
AU - Krebbers, Robbert
AU - Visser, Eelco
PY - 2020
Y1 - 2020
N2 - 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
AB - 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
KW - Agda
KW - Definitional interpreters
KW - Dependent types
KW - Linear types
KW - Mechanized semantics
KW - Separation logic
KW - Session types
KW - Type safety
UR - http://www.scopus.com/inward/record.url?scp=85079464050&partnerID=8YFLogxK
U2 - 10.1145/3372885.3373818
DO - 10.1145/3372885.3373818
M3 - Working paper
SP - 284
EP - 298
BT - Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
PB - ACM DL
ER -