Reference. The Interval Domain in Homotopy Type Theory
Cite
Cited by (1)
Initial Algebras of Domains via Quotient Inductive-Inductive Types vancollem-2025-initial
Domain theory has been developed as a mathematical theory of computation and to give a denotational semantics to programming languages. It helps us to fix the meaning of language concepts, to understand how programs behave and to reason about programs. At the same time it serves as a great theory to model various algebraic effects such as non-determinism, partial functions, side effects and numerous other forms of computation. In the present paper, we present a general framework to construct algebraic effects in domain theory, where our domains are DCPOs: directed complete partial orders. We first describe so called DCPO algebras for a signature, where the signature specifies the operations on the DCPO and the inequational theory they obey. This provides a method to represent various algebraic effects, like partiality. We then show that initial DCPO algebras exist by defining them as so called Quotient Inductive-Inductive Types (QIITs), known from homotopy type theory. A quotient inductive-inductive type allows one to simultaneously define an inductive type and an inductive relation on that type, together with equations on the type. We illustrate our approach by showing that several well-known constructions of DCPOs fit our framework: coalesced sums, smash products and free DCPOs (partiality and power domains). Our work makes use of various features of homotopy type theory and is formalized in Cubical Agda.
Cites 35 works (1 here)
External (34)
- Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics (2024)
- Symmetric Monoidal Smash Products in Homotopy Type Theory (2024)
- Apartness, sharp elements, and the Scott topology of domains (2023)
- Domain theory in constructive and predicative univalent foundations (PhD thesis) (2023)
- Synthetic topology in Homotopy Type Theory for probabilistic programming (2021)
- Extensional constructive real analysis via locators (2021)
- The Scott model of PCF in univalent type theory (2021)
- Sharp Elements and Apartness in Domains (2021)
- Global Optimisation with Constructive Reals (2021)
- Domain theory in constructive and predicative univalent foundations (2021)
- The HoTT reals coincide with the Escardó-Simpson reals (2017)
- Formalization of real analysis: a survey of proof assistants and libraries (2016)
- Formalising real numbers in homotopy type theory (2016)
- Type classes for efficient exact real arithmetic in Coq (2013)
- Proofs of randomized algorithms in Coq (2009)
- A constructive theory of continuous domains suitable for implementation (2009)
- The Dedekind reals in abstract Stone duality (2009)
- Certified exact transcendental real number computation in Coq (2008)
- Constructive analysis, types and exact real numbers (2007)
- A monadic, functional implementation of real numbers (2007)
- The constructive maximal point space and partial metrizability (2006)
- C-CoRN, the constructive Coq repository at Nijmegen (2004)
- On the non-sequential nature of the interval-domain model of real-number computation (2004)
- Higher Operads, Higher Categories (2003)
- A Constructive Formalization of the Fundamental Theorem of Calculus (2003)
- Constructive Reals in Coq: Axioms and Categoricity (2002)
- A co-inductive approach to real numbers (2000)
- Induction and recursion on the partial real line with applications to Real PCF (1999)
- PCF extended with real numbers (1996)
- Domain Theory (1995)
- Completing the rationals and metric spaces in LEGO (1993)
- Constructive Analysis (1985)
- Foundations of Constructive Analysis (1967)
- UniMath — a computer-checked library of univalent mathematics