Intrinsically-Typed Language Fragments

Cas van der Rest


Date: Wed, May 11, 2022
Time: 12:00
Room: Turing 0.E420


Intrinsically-typed interpreters are an attractive approach for verifying type safety: one specifies the operational semantics of the object language by writing an interpreter in a dependently-typed host language, and type checker verifies that this semantics is type safe. This approach, however, relies on (indexed) data types and pattern matching functions, which require the entirety of a language’s syntax and semantics to be defined at once. Consequently, we cannot reuse (parts of) a specification without copying or re-typechecking existing code. In this talk, we discuss how to define language fragments that are both intrinsically typed and intrinsically composable. Such language fragments form a self-contained partial specification of language’s syntax and semantics that is safe by construction and composable by design. Additionally, language fragments are closed under a composition operation that preserves safety and composability, allowing for type safe language specifications to be assembled by composing multiple fragments.

Previous: |
Next: |