An intrinsically-typed interpreter is an implementation of the semantics of a programming language. A key feature of intrinsically-typed interpreters is that the type of the interpreter represents the type safety theorem of the object language.

We are developing intrinsically-typed interpreters for languages with effects and coeffects. Our aim is to find general abstractions for hiding proof terms and thus enable concise implementation of effectful and coeffectful languages. At the workshop, we intend to discuss with the participants what kind of abstractions would be useful, as well as how to implement those abstractions.