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

DOI10.2168/LMCS-8(4:1)2012MaRDI QIDQ3166222zbMATHOpenAlexFDO

Authors Rasmus Ejlers Møgelberg, Kristian Støvring, Lars Birkedal, Jan Schwinghammer

Publication date 22 October 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1208.3596

zbMATH Keywords

programming languagesdependent typesdenotational semanticsrecursive typesHeyting algebraprogram logicsinternal logicstep-indexed modelsguarded recursionaxiomatic categorical treatmentsynthetic guarded domain theory

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Categorical logic, topoi (03G30) Topoi (18B25) Semantics in the theory of computing (68Q55)

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

(41)

• Adjoint reactive GUI programming
• Temporal refinements for guarded recursive types
• A formal logic for formal category theory
• Deciding Equations in the Time Warp Algebra
• A ghost at \(\omega_1\)
• A metalanguage for guarded iteration
• Two guarded recursive powerdomains for applicative simulation
• Modal FRP for all: Functional reactive programming without space leaks in Haskell
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Coinduction in Flow: The Later Modality in Fibrations
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Modal dependent type theory and dependent right adjoints
• Lewis meets Brouwer: constructive strict implication
• scientific article; zbMATH DE number 7288622 (Why is no real title available?)
• A model of PCF in guarded type theory
• scientific article; zbMATH DE number 7566072 (Why is no real title available?)
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Monoidal streams for dataflow programming
• A model of countable nondeterminism in guarded type theory
• Constructive modalities with provability smack
• Step-indexed Kripke models over recursive worlds
• Monoidal-closed categories of tree automata
• Guarded dependent type theory with coinductive types
• Formally verifying exceptions for low-level code with separation logic
• Transpension: the right adjoint to the Pi-type
• Multimodal dependent type theory
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• Denotational semantics for guarded dependent type theory
• What should a generic object be?
• scientific article; zbMATH DE number 7559298 (Why is no real title available?)
• Transfinite step-indexing: decoupling concrete and logical steps
• Denotational semantics of recursive types in synthetic guarded domain theory
• The clocks they are adjunctions. Denotational semantics for clocked type theory
• scientific article; zbMATH DE number 7204446 (Why is no real title available?)
• Guarded cubical type theory
• A model of guarded recursion with clock synchronisation
• On models of higher-order separation logic
• Towards a common categorical semantics for linear-time temporal logic and functional reactive programming
• A model of guarded recursion via generalised equilogical spaces
• Time warps, from algebra to algorithms
• scientific article; zbMATH DE number 7243672 (Why is no real title available?)

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)