6 citations · 16 across the 11 of their papers we have counts for
4 papers · 1 filter
Examples and counterexamples of injective types
Tom de Jong, Martín Hötzel Escardó
It is known that, in univalent mathematics, type universes, the type of -types in a universe, reflective subuniverses, and the underlying type of any algebra of the lifting mona…
Apartness, sharp elements, and the Scott topology of domains
Tom de Jong
Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology. Our two primary novelties are a notion of intrinsic apartness and a notion of s…
Domain Theory in Constructive and Predicative Univalent Foundations
Tom de Jong, Martín Hötzel Escardó
We develop domain theory in constructive univalent foundations without Voevodsky's resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and pr…
The Scott model of PCF in univalent type theory
Tom de Jong
We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF,…