A relational model of types-and-effects in higher-order concurrent separation logic. - Morten Krogh-Jespersen; Kasper Svendsen; Lars Birkedal (POPL, 2017)

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. - Amin Timany; Léo Stefanesco; Morten Krogh-Jespersen; Lars Birkedal (Proc. ACM Program. Lang., 2018)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. - Morten Krogh-Jespersen; Amin Timany; Marit Edna Ohlenbusch; Simon Oddershede Gregersen; Lars Birkedal (ESOP, 2020)