Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks

Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi

Guarded recursion is a powerful modal approach to recursion that can be seen as an abstract form of step-indexing. It is currently used extensively in separation logic to model pro…