Domain theory in constructive and predicative univalent foundations

Tom De Jong, Martin Escardo

Research output: Chapter in Book/Report/Conference proceedingConference contribution

58 Downloads (Pure)


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 proved its computational adequacy, based on directed complete posets (dcpos). Here we further consider algebraic and continuous dcpos, and construct Scott’s D model of the untyped λ-calculus. A common approach to deal with size issues in a predicative foundation is to work with information systems or abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. Here we instead accept that dcpos may be large and work with type universes to account for this. For instance, in the Scott model of PCF, the dcpos have carriers in the second universe U1 and suprema of directed families with indexing type in the first universe U0. Seeing a poset as a category in the usual way, we can say that these dcpos are large, but locally small, and have small filtered colimits. In the case of algebraic dcpos, in order to deal with size issues, we proceed mimicking the definition of accessible category. With such a definition, our construction of Scott’s D again gives a large, locally small, algebraic dcpo with small directed suprema.

Original languageEnglish
Title of host publication29th EACSL Annual Conference on Computer Science Logic, CSL 2021
EditorsChristel Baier, Jean Goubault-Larrecq
PublisherSchloss Dagstuhl
Number of pages18
ISBN (Electronic)9783959771757
Publication statusPublished - 13 Jan 2021
Event29th EACSL Annual Conference on Computer Science Logic - Held Online Due to COVID-19, Ljubljana, Slovenia
Duration: 25 Jan 202128 Jan 2021

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
ISSN (Electronic)1868-8969


Conference29th EACSL Annual Conference on Computer Science Logic
Abbreviated titleCSL 2021
Internet address

Bibliographical note

Publisher Copyright:
© Tom de Jong and Martín Hötzel Escardó.


  • Constructivity
  • Domain theory
  • Predicativity
  • Univalent foundations

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Domain theory in constructive and predicative univalent foundations'. Together they form a unique fingerprint.

Cite this