7 votes

An analogue of Scott continuity for infinite-time-Turing-computable functions

The domain-theoretic considerations of the kind you are asking about can be carried out using synthetic domain theory. Related to it is syntehtic topology, and in fact the two share many common ideas. ...
  • 26.8k
6 votes
Accepted

Is there an isomorphism between universal domains $\mathcal{P}\omega$ and the interval domain $\mathbf{I}\mathbb{R}$?

This is only half an answer, but allow me to clear up a constructive point about the interval domain. The usual definition of the interval domain is $$\mathrm{I}\mathbb{R} = \{[a,b] \mid a, b \in \...
  • 26.8k
4 votes
Accepted

Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

Let me first say that I did not look carefully at the second part of your question, nor your sketch of why the clock quantifier should commute with propositional existential quantification. I will ...
2 votes

Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

This question sounds related to Transfinite Iris, which proposes to change the Iris model from Nat-indexed propositions to Ordinal-indexed propositions to have "later" commute with ...
  • 1,910

Only top scored, non community-wiki answers of a minimum length are eligible