The Scott model of PCF in univalent type theory

Tom De Jong

Research output: Contribution to journalArticlepeer-review

101 Downloads (Pure)


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, we use the lifting monad (also known as the partial map classifier monad) from topos theory, which has been extended to univalent type theory by Escardó and Knapp. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or quotient inductive-inductive types. We show that one can do without these extensions.
Original languageEnglish
JournalMathematical Structures in Computer Science
Early online date23 Jul 2021
Publication statusE-pub ahead of print - 23 Jul 2021

Bibliographical note

Publisher Copyright:
© The Author(s), 2021. Published by Cambridge University Press.


  • Lifting monad
  • Partial map classifier
  • Pcf
  • Scott model
  • Type theory
  • Univalent mathematics

ASJC Scopus subject areas

  • Mathematics (miscellaneous)
  • Computer Science Applications


Dive into the research topics of 'The Scott model of PCF in univalent type theory'. Together they form a unique fingerprint.

Cite this