A denotationally-based program logic for higher-order store. - Frederik Lerbjerg Aagaard; Jonathan Sterling; Lars Birkedal (MFPS, 2023)

Unifying cubical and multimodal type theory. - Frederik Lerbjerg Aagaard; Magnus Baunsgaard Kristensen; Daniel Gratzer; Lars Birkedal (Log. Methods Comput. Sci., 2024)