A model of Clocked Cubical Type Theory. - Magnus Baunsgaard Kristensen; Rasmus Ejlers Møgelberg; Andrea Vezzosi (CoRR, 2021)

Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. - Magnus Baunsgaard Kristensen; Rasmus Ejlers Møgelberg; Andrea Vezzosi (LICS, 2022)

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