First steps in synthetic guarded domain theory: step-indexing in the topos of trees
From MaRDI portal
(Redirected from Publication:3166222)
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.
Recommendations
- A model of guarded recursion via generalised equilogical spaces
- Denotational semantics of recursive types in synthetic guarded domain theory
- A model of countable nondeterminism in guarded type theory
- Denotational semantics of recursive types in synthetic guarded domain theory
- Two models of synthetic domain theory
Cited in
(47)- Formally verifying exceptions for low-level code with separation logic
- Lewis meets Brouwer: constructive strict implication
- A model of guarded recursion via generalised equilogical spaces
- On models of higher-order separation logic
- Adjoint reactive GUI programming
- Temporal refinements for guarded recursive types
- Guarded cubical type theory
- Time warps, from algebra to algorithms
- Transfinite step-indexing: decoupling concrete and logical steps
- Guarded dependent type theory with coinductive types
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Towards a common categorical semantics for linear-time temporal logic and functional reactive programming
- A ghost at _1
- Denotational semantics of recursive types in synthetic guarded domain theory
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- The clocks they are adjunctions. Denotational semantics for clocked type theory
- Guarded recursion in Agda via sized types
- \textbf{Actris 2.0}: asynchronous session-type based reasoning in separation logic
- scientific article; zbMATH DE number 7204446 (Why is no real title available?)
- Dual-context calculi for modal logic
- Denotational semantics for guarded dependent type theory
- scientific article; zbMATH DE number 7288622 (Why is no real title available?)
- Multimodal dependent type theory
- A model of countable nondeterminism in guarded type theory
- Monoidal-closed categories of tree automata
- Modal dependent type theory and dependent right adjoints
- Constructive modalities with provability smack
- Step-indexed Kripke models over recursive worlds
- Coinduction in Flow: The Later Modality in Fibrations
- A metalanguage for guarded iteration
- A model of guarded recursion with clock synchronisation
- A model of PCF in guarded type theory
- scientific article; zbMATH DE number 7779294 (Why is no real title available?)
- A formal logic for formal category theory
- Modal FRP for all: Functional reactive programming without space leaks in Haskell
- Deciding Equations in the Time Warp Algebra
- What should a generic object be?
- Transpension: the right adjoint to the Pi-type
- Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
- Monoidal streams for dataflow programming
- Two guarded recursive powerdomains for applicative simulation
- What monads can and cannot do with a bit of extra time
- Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
- What monads can and cannot do with a few extra pages
- Two-dimensional Kripke semantics i: presheaves
- Idempotent resources in separation logic. The heart of \texttt{core} in Iris
- Unifying cubical and multimodal type theory
This page was built for publication: First steps in synthetic guarded domain theory: step-indexing in the topos of trees
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3166222)
