Scopes as types. - Hendrik van Antwerpen; Casper Bach Poulsen; Arjen Rouvoet; Eelco Visser (Proc. ACM Program. Lang., 2018)

Intrinsically-typed definitional interpreters for imperative languages. - Casper Bach Poulsen; Arjen Rouvoet; Andrew Tolmach; Robbert Krebbers; Eelco Visser (Proc. ACM Program. Lang., 2018)

Intrinsically-typed definitional interpreters for linear, session-typed languages. - Arjen Rouvoet; Casper Bach Poulsen; Robbert Krebbers; Eelco Visser (CPP, 2020)

Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications. - Arjen Rouvoet; Hendrik van Antwerpen; Casper Bach Poulsen; Robbert Krebbers; Eelco Visser (Proc. ACM Program. Lang., 2020)

Intrinsically typed compilation with nameless labels. - Arjen Rouvoet; Robbert Krebbers; Eelco Visser (Proc. ACM Program. Lang., 2021)

Correct by Construction Language Implementations. - Arjen Rouvoet (2021)

Intrinsically-typed definitional interpreters à la carte. - Cas van der Rest; Casper Bach Poulsen; Arjen Rouvoet; Eelco Visser; Peter D. Mosses (Proc. ACM Program. Lang., 2022)