Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion

Reference. Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion

Several different topoi have played an important role in the development and applications of synthetic guarded domain theory (SGDT), a new kind of synthetic domain theory that abstracts the concept of guarded recursion frequently employed in the semantics of programming languages. In order to unify the accounts of guarded recursion and coinduction, several authors have enriched SGDT with multiple “clocks” parameterizing different time-streams, leading to more complex and difficult to understand topos models. Until now these topoi have been understood very concretely qua categories of presheaves, and the logico-geometrical question of what theories these topoi classify has remained open. We show that several important topos models of SGDT classify very simple geometric theories, and that the passage to various forms of multi-clock guarded recursion can be rephrased more compositionally in terms of the lower bagtopos construction of Vickers and variations thereon due to Johnstone. We contribute to the consolidation of SGDT by isolating the universal property of multi-clock guarded recursion as a modular construction that applies to any topos model of single-clock guarded recursion.

Cite

Cite as @palombi_sterling_2023 (helia, typst) · \cite{palombi_sterling_2023} (LaTeX)

BibTeX

bibtex · 9 lines

@article{palombi_sterling_2023,
 title = {Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion},
 author = {Palombi, Daniele and Sterling, Jonathan},
 year = {2023},
 journal = {Electronic Notes in Theoretical Informatics and Computer Science},
 volume = {1},
 note = {MFPS XXXVIII; arXiv:2210.04636},
 url = {https://arxiv.org/abs/2210.04636}
}

hayagriva YAML (typst)

yaml · 13 lines

palombi_sterling_2023:
  type: article
  title: 'Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion'
  author:
  - Palombi, Daniele
  - Sterling, Jonathan
  date: 2023
  url: https://arxiv.org/abs/2210.04636
  note: MFPS XXXVIII; arXiv:2210.04636
  parent:
    type: periodical
    title: Electronic Notes in Theoretical Informatics and Computer Science
    volume: 1

Download: palombi_sterling_2023.bib · palombi_sterling_2023.yml

Cites 55 works (6 here)

With notes (6)

Quotients, inductive types, and quotient inductive types fiore-2022-quotientsLMCS · 2022

This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.

DOI · arXiv

A Stratified Approach to Löb Induction gratzer-2022-aFSCD · 2022

Guarded type theory extends type theory with a handful of modalities and constants to encode productive recursion. While these theories have seen widespread use, the metatheory of guarded type theories, particularly guarded dependent type theories remains underdeveloped. We show that integrating Löb induction is the key obstruction to unifying guarded recursion and dependence in a well-behaved type theory and prove a no-go theorem sharply bounding such type theories. Based on these results, we introduce GuTT: a stratified guarded type theory. GuTT is properly two type theories, sGuTT and dGuTT. The former contains only propositional rules governing Löb induction but enjoys decidable type-checking while the latter extends the former with definitional equalities. Accordingly, dGuTT does not have decidable type-checking. We prove, however, a novel guarded canonicity theorem for dGuTT, showing that programs in dGuTT can be run. These two type theories work in concert, with users writing programs in sGuTT and running them in dGuTT.

DOI

First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory sterling_20212021

The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits the universal properties of their syntactic categories to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory inform the design and implementation of correct-by-construction elaboration algorithms, promising a principled interface between real proof assistants and ideal mathematics. In this dissertation, I add synthetic Tait computability to the arsenal of the objective metatheorist. Synthetic Tait computability is a mathematical machine to reduce difficult problems of type theory and programming languages to trivial theorems of topos theory. First employed by Sterling and Harper to reconstruct the theory of program modules and their phase separated parametricity, synthetic Tait computability is deployed here to resolve the last major open question in the syntactic metatheory of cubical type theory: normalization of open terms.

DOI

Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018JFP · 2018

Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.

PDF · DOI · pldb

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning jung-2015-irisPOPL · 2015

PDF · DOI · pldb

Productive coprogramming with guarded recursion atkey-2013-productiveICFP · 2013

PDF · DOI · pldb

External (49)

Greatest hits: Higher inductive types in coinductive definitions via induction under clocks (2022)
Topo-logie (2021)
Idris 2: Quantitative Type Theory in Practice (2021)
Denotational semantics for guarded dependent type theory (2020)
Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory (2020)
Formalizing pi-calculus in Guarded Cubical Agda (2020)
A model of guarded recursion via generalised equilogical spaces (2018)
On models of higher-order separation logic (2018)
Guarded Computational Type Theory (2018)
The clocks are ticking: No more delays! (2017)
Guarded dependent type theory with coinductive types (2016)
The Coq Proof Assistant Reference Manual (2016)
Denotational semantics of recursive types in synthetic guarded domain theory (2016)
Denotational semantics in Synthetic Guarded Domain Theory (2016)
A model of guarded recursion with clock synchronisation (2015)
A model of PCF in Guarded Type Theory (2015)
A type theory for productive coprogramming via guarded recursion (2014)
Intensional type theory with guarded recursive types qua fixed points on universes (2013)
Idris, a general-purpose dependently typed programming language: Design and implementation (2013)
Fibred 2-categories and bicategories (2013)
First steps in synthetic guarded domain theory: Step-indexing in the topos of trees (2011)
A metric model of lambda calculus with guarded recursion (2010)
The category-theoretic solution of recursive metric-space equations (2010)
Realisability semantics of parametric polymorphism, general references and recursive types (2010)
Towards a practical programming language based on dependent type theory (2007)
Singular coverings of toposes (2006)
Synthetic Differential Geometry (2006)
Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2 (2002)
Wellfounded trees in categories (2000)
A modality for recursion (2000)
A metric model of PCF (1999)
Topical categories of domains (1999)
Spreads and the symmetric topos II (1998)
Spreads and the symmetric topos (1996)
Proving the correctness of reactive systems using sized types (1996)
Intuitionistic sets and ordinals (1996)
Solving domain equations in a category of compact metric spaces (1994)
Variations on the bagdomain theme (1994)
Partial products, bagdomains and hyperlocal toposes (1992)
On the foundation of final semantics: Non-standard sets, metric spaces, partial orders (1992)
Geometric theories and databases (1992)
First steps in synthetic domain theory (1991)
Solving reflexive domain equations in a category of complete metric spaces (1987)
An ideal model for recursive polymorphic types (1984)
Domains for denotational semantics (1982)
A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on (1980)
Data types as lattices (1976)
Change of base for toposes with generators (1975)
Outline of a mathematical theory of computation (1970)