Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
| Autor: | Eelco Visser, Casper Bach Poulsen, Arjen Rouvoet, Robbert Krebbers |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Computer science
Semantics (computer science) Agda Concurrency Definitional interpreters Session types 02 engineering and technology Separation logic computer.software_genre Mechanized semantics Type safety 0202 electrical engineering electronic engineering information engineering Linear types computer.programming_language Programming language 020207 software engineering computer.file_format Object (computer science) Dependent types Computer Science::Programming Languages 020201 artificial intelligence & image processing Executable computer Interpreter |
| Zdroj: | CPP |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|