Reference. The Interval Domain in Homotopy Type Theory

Niels van der Weide, Dan Frumin · · homotopy-type-theory · DOI

Cite

Cite as @vanderweide-2024-the (helia, typst) · \cite{vanderweide-2024-the} (LaTeX)
BibTeX
bibtex · 1 line
@inbook{vanderweide-2024-the, title={The Interval Domain in Homotopy Type Theory}, ISBN={9783031617164}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-031-61716-4_16}, DOI={10.1007/978-3-031-61716-4_16}, booktitle={Logics and Type Systems in Theory and Practice}, publisher={Springer Nature Switzerland}, author={van der Weide, Niels and Frumin, Dan}, year={2024}, pages={241–256} }
hayagriva YAML (typst)
yaml · 19 lines
vanderweide-2024-the:
  type: chapter
  title: The Interval Domain in Homotopy Type Theory
  author:
  - name: Weide
    given-name: Niels
    prefix: van der
  - Frumin, Dan
  date: 2024
  page-range: 241-256
  url: http://dx.doi.org/10.1007/978-3-031-61716-4_16
  serial-number:
    doi: 10.1007/978-3-031-61716-4_16
    isbn: '9783031617164'
    issn: 1611-3349
  parent:
    type: book
    title: Logics and Type Systems in Theory and Practice
    publisher: Springer Nature Switzerland
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.
DOI
Cites 35 works (1 here)
With notes (1)

Homotopy Type Theory: Univalent Foundations of Mathematics hottbook

Web · arXiv
External (34)
vanderweide-2024-the reference entries/refs/vanderweide-2024-the/vanderweide-2024-the.hel