First steps in synthetic guarded domain theory: step-indexing in the topos of trees

Abstract

We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show how to solve recursive type equations involving dependent types. We propose that the internal logic of S provides the right setting for the synthetic construction of abstract versions of step-indexed models of programming languages and program logics. As an example, we show how to construct a model of a programming language with higher-order store and recursive types entirely inside the internal logic of S. Moreover, we give an axiomatic categorical treatment of models of synthetic guarded domain theory and prove that, for any complete Heyting algebra A with a well-founded basis, the topos of sheaves over A forms a model of synthetic guarded domain theory, generalizing the results for S.

Cited by in corpus (19)

• Constructive Modalities with Provability Smack
• A Generalized Modality for Recursion
• Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic
• Guarded Cubical Type Theory: Path Equality for Guarded Recursion
• Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion
• Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
• Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion
• Two Guarded Recursive Powerdomains for Applicative Simulation
• Categorical Semantics for Functional Reactive Programming with Temporal Recursion and Corecursion
• Almost-Sure Termination by Guarded Refinement
• Transpension: The Right Adjoint to the Pi-type
• A Metalanguage for Guarded Iteration
• Sikkel: Multimode Simple Type Theory as an Agda Library
• Ruitenburg's Theorem Mechanized and Contextualized
• Unifying cubical and multimodal type theory
• A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures
• Sequent Calculus in the Topos of Trees
• Multimodal Dependent Type Theory
• Endofunctors modelling higher-order behaviours