Abstract
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 language | English |
---|---|
Journal | Mathematical Structures in Computer Science |
Early online date | 23 Jul 2021 |
DOIs | |
Publication status | E-pub ahead of print - 23 Jul 2021 |
Bibliographical note
Publisher Copyright:© The Author(s), 2021. Published by Cambridge University Press.
Keywords
- Lifting monad
- Partial map classifier
- Pcf
- Scott model
- Type theory
- Univalent mathematics
ASJC Scopus subject areas
- Mathematics (miscellaneous)
- Computer Science Applications