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

DOI10.2168/LMCS-8(4:1)2012zbMATH Open1269.03035arXiv1208.3596OpenAlexW2020900140MaRDI QIDQ3166222FDOQ3166222

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)

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.

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

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

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)

Cited In (40)

• Guarded Dependent Type Theory with Coinductive Types
• Denotational semantics of recursive types in synthetic guarded domain theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Monoidal-closed categories of tree automata
• Transpension: the right adjoint to the Pi-type
• Title not available (Why is that?)
• On models of higher-order separation logic
• Title not available (Why is that?)
• Deciding Equations in the Time Warp Algebra
• Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming
• A Light Modality for Recursion
• What should a generic object be?
• Adjoint reactive GUI programming
• Temporal refinements for guarded recursive types
• Guarded cubical type theory
• A formal logic for formal category theory
• Coinduction in Flow: The Later Modality in Fibrations
• Title not available (Why is that?)
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Title not available (Why is that?)
• Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
• Constructive Modalities with Provability Smack
• Title not available (Why is that?)
• A metalanguage for guarded iteration
• A model of guarded recursion with clock synchronisation
• Title not available (Why is that?)
• 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
• Formally verifying exceptions for low-level code with separation logic
• Two guarded recursive powerdomains for applicative simulation
• Lewis meets Brouwer: constructive strict implication
• Denotational semantics for guarded dependent type theory
• Title not available (Why is that?)
• Modal dependent type theory and dependent right adjoints
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Time warps, from algebra to algorithms
• A model of guarded recursion via generalised equilogical spaces
• 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)