Intrinsically-Typed Interpreters

An intrinsically-typed interpreter is an interpreter of language A written in language B, where type-safety of A’s program is guaranteed by means of the type system of B. We are developing intrinsically-typed interpreters for languages with advanced language features such as effects, coeffects, and control operators. Our aim is to find general abstractions for hiding proof terms and thus enable concise implementations.

News