English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We develop domain theory in constructive and predicative univalentfoundations (also known as homotopy type theory). That we work predicativelymeans that we do not assume Voevodsky's propositional resizing axioms. Our workis constructive in the sense that we do not rely on excluded middle or theaxiom of (countable) choice. Domain theory studies so-called directed completeposets (dcpos) and Scott continuous maps between them and has applications inprogramming language semantics, higher-type computability and topology. Acommon approach to deal with size issues in a predicative foundation is to workwith information systems, abstract bases or formal topologies rather thandcpos, and approximable relations rather than Scott continuous functions. Inour type-theoretic approach, we instead accept that dcpos may be large and workwith type universes to account for this. A priori one might expect that complexconstructions of dcpos result in a need for ever-increasing universes and arepredicatively impossible. We show that such constructions can be carried out ina predicative setting. We illustrate the development with applications in thesemantics of programming languages: the soundness and computational adequacy ofthe Scott model of PCF and Scott's $D_\infty$ model of the untyped$\lambda$-calculus. We also give a predicative account of continuous andalgebraic dcpos, and of the related notions of a small basis and its roundedideal completion. The fact that nontrivial dcpos have large carriers is in factunavoidable and characteristic of our predicative setting, as we explain in acomplementary chapter on the constructive and predicative limitations ofunivalent foundations. Our account of domain theory in univalent foundations isfully formalised with only a few minor exceptions. The ability of the proofassistant Agda to infer universe levels has been invaluable for our purposes.

Domain Theory in Constructive and Predicative Univalent Foundations