A relational modal logic for higher-order stateful ADTs. - Derek Dreyer; Georg Neis; Andreas Rossberg; Lars Birkedal (POPL, 2010)

Self-adjusting stack machines. - Matthew A. Hammer; Georg Neis; Yan Chen 001; Umut A. Acar (OOPSLA, 2011)

Non-parametric parametricity. - Georg Neis; Derek Dreyer; Andreas Rossberg (J. Funct. Program., 2011)

The marriage of bisimulations and Kripke logical relations. - Chung-Kil Hur; Derek Dreyer; Georg Neis; Viktor Vafeiadis (POPL, 2012)

The impact of higher-order state and control effects on local relational reasoning. - Derek Dreyer; Georg Neis; Lars Birkedal (J. Funct. Program., 2012)

The power of parameterization in coinductive proof. - Chung-Kil Hur; Georg Neis; Derek Dreyer; Viktor Vafeiadis (POPL, 2013)

Pilsner: a compositionally verified compiler for a higher-order imperative language. - Georg Neis; Chung-Kil Hur; Jan-Oliver Kaiser; Craig McLaughlin; Derek Dreyer; Viktor Vafeiadis (ICFP, 2015)

Compositional compiler correctness via parametric simulations. - Georg Neis (2018)