Decidability of conversion for type theory in type theory. - Andreas Abel 001; Joakim Öhman; Andrea Vezzosi (Proc. ACM Program. Lang., 2018)

Visibility reasoning for concurrent snapshot algorithms. - Joakim Öhman; Aleksandar Nanevski (Proc. ACM Program. Lang., 2022)