The introduction of this paper could be a start for guarded lamdba calculus/ guarded recursion: https://arxiv.org/abs/1606.09455

]]>So we’d perhaps need a page for ’guarded recursion’ first? Would that be a starting point for entries involving guardedness?

]]>I think we can have a separate page on guarded dependent type theory. It has more applications than just synthetic domain theory. I can try to collect some references. We recently wrote a paper on guarded cubical type theory, which I’ll add to cubical type theory. https://arxiv.org/abs/1611.09263.

Ales Bizjak, now a postdoc in our group, recently completed his PhD thesis on guarded recursion. It includes a long introduction to the subject. http://www.cs.au.dk/~abizjak/documents/thesis/semantics-applications-gr.pdf

]]>I just went to a talk on this next door in our Computer Science dept. by Marco Paviotti. He’s recently joined Kent after finishing a PhD, Denotational semantics in Synthetic Guarded Domain Theory. Coincidently Bas just pointed me to a paper co-authored by Marco’s supervisor First steps in synthetic guarded domain theory: step-indexing in the topos of trees.

We don’t have a great deal in this area. What can we add to domain theory?

]]>