The Scott model of PCF in univalent type theory

DOI10.1017/S0960129521000153OpenAlexW3174840905MaRDI QIDQ5055497

Tom J. de Jong

Publication date: 9 December 2022

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1904.09810

zbMATH Keywords

type theoryPCFpartial map classifierunivalent mathematicslifting monadScott model

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• UniMath
• GitHub

Cites Work

• LCF considered as a programming language
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• Partiality, Revisited
• Some Domain Theory and Denotational Semantics in Coq
• Domain-Theoretic Foundations of Functional Programming
• General synthetic domain theory – a logical approach
• Quotienting the delay monad by weak bisimilarity
• Partial Elements and Recursion via Dominances in Univalent Type Theory.
• General Recursion via Coinductive Types
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Predicative Aspects of Order Theory in Univalent Foundations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item