Models of Intrinsically-Typed Effects
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.

This style of specification is particularly challenging for languages with side effects, like exceptions or mutable state. While recent work by Bach Poulsen et al. (2017) and Rouvoet et al. (2020) has extended the approach to imperative and session-typed languages, the state of the art in intrinsically-typed interpreters still lacks a uniform way of dealing with these side effects.

In this project, we investigate how effects and handlers (Plotkin and Power, 2003; Plotkin and Pretnar, 2009) can be applied to define intrinsically-typed effects, and we will work towards finding a model describes the different known instances.

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.
  • Plotkin, G., & Power, J. (2003). Algebraic operations and generic effects. Applied categorical structures, 11(1), 69-94.
  • Plotkin, G., & Pretnar, M. (2009, March). Handlers of algebraic effects. In European Symposium on Programming (pp. 80-94). Springer, Berlin, Heidelberg.
  • 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


Models of Intrinsically-Typed Effects

Supervisor(s): Cas van der Rest, Casper Bach Poulsen
Posted: May 11, 2022