Denotational semantics of recursive types in synthetic guarded domain theory
Rasmus Ejlers Møgelberg, Marco Paviotti · 2016
Guarded recursion is a form of recursion where recursive calls are guarded by delay modalities. Previous work has shown how guarded recursion is useful for reasoning operationally about programming languages with advanced features including general references, recursive types, countable non-determinism and concurrency.