Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 4 of 4
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?
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
So we’d perhaps need a page for ’guarded recursion’ first? Would that be a starting point for entries involving guardedness?
The introduction of this paper could be a start for guarded lamdba calculus/ guarded recursion: https://arxiv.org/abs/1606.09455
1 to 4 of 4