Programming and Reasoning with Guarded Recursion for Coinductive Types. - Ranald Clouston; Ales Bizjak; Hans Bugge Grathwohl; Lars Birkedal (FoSSaCS, 2015)

Guarded Cubical Type Theory: Path Equality for Guarded Recursion. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (CSL, 2016)

Guarded Dependent Type Theory with Coinductive Types. - Ales Bizjak; Hans Bugge Grathwohl; Ranald Clouston; Rasmus Ejlers Møgelberg; Lars Birkedal (FoSSaCS, 2016)

The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. - Ranald Clouston; Ales Bizjak; Hans Bugge Grathwohl; Lars Birkedal (Log. Methods Comput. Sci., 2016)

The clocks are ticking: No more delays! - Patrick Bahr; Hans Bugge Grathwohl; Rasmus Ejlers Møgelberg (LICS, 2017)

Guarded Cubical Type Theory. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (J. Autom. Reason., 2019)