Intrinsically-Typed Specifications for Type-and-Effect Systems
Master Project

Project Description

In dependently-typed programming languages, we can specify the operational semantics of other programming languages by writing a so-called intrinsically-typed definitional interpreter(Augustsson and Carlsson, 1999). The key idea is to specify the run-time behaviour of a language by writing an interpreter that defines its operational semantics, but by using the power of dependent types we can assign a very precise type to this interpreter that allows the host language’s type checker to simultaneously assert that it defines a type sound semantics.

In recent work, Bach Poulsen et al. (2017) and Rouvoet et al. (2020) extended the approach to imperative and session-typed languages. Still, for many common language features it is still an open question how to write intrinsically-typed specifications.

In this project, we will work towards defining intrinsically-typed specifications for a broader class of languages. In particular, we will investigate how to write specifications for languages with type-and-effect systems, where in addition to a program’s type we also statically approximate its side effects. A potential starting point for this project could the work by Mycroft et al. (2016), who define a semantics for a broad class of type and effect systems.

Requirements

• Some experience with programming with dependent types (e.g., in Agda), and functional programming in general.

Relevant literature:

• Augustsson, L., & Carlsson, M. (1999). An exercise in dependent types: A well-typed interpreter. In Workshop on Dependent Types in Programming, Gothenburg.
• Mycroft, A., Orchard, D., & Petricek, T. (2016). Effect systems revisited—control-flow algebra and semantics. In Semantics, Logics, and Calculi (pp. 1-32). Springer, Cham.
• Bach Poulsen, C., Rouvoet, A., Tolmach, A., Krebbers, R., & Visser, E. (2017). Intrinsically-typed definitional interpreters for imperative languages. Proceedings of the ACM on Programming Languages, 2(POPL), 1-34.
• Rouvoet, A., Bach Poulsen, C., Krebbers, R., & Visser, E. (2020, January). Intrinsically-typed definitional interpreters for linear, session-typed languages. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 284-298).

Contacts for the project

• Cas van der Rest (TU Delft)
• Casper Bach Poulsen (TU Delft)