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

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

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)

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

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)