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

DOI10.2168/LMCS-8(4:1)2012zbMath1269.03035arXiv1208.3596OpenAlexW2020900140MaRDI QIDQ3166222

Kristian Støvring, Rasmus Ejlers Møgelberg, 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 languagesHeyting algebradenotational semanticsdependent typesrecursive typesprogram logicsinternal logicstep-indexed modelsguarded recursionaxiomatic categorical treatmentsynthetic guarded domain theory

Mathematics Subject Classification ID

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

Related Items (36)

On models of higher-order separation logic ⋮ Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming ⋮ Formally verifying exceptions for low-level code with separation logic ⋮ Unnamed Item ⋮ Lewis meets Brouwer: constructive strict implication ⋮ 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? ⋮ Time warps, from algebra to algorithms ⋮ A model of guarded recursion via generalised equilogical spaces ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ Unnamed Item ⋮ A model of guarded recursion with clock synchronisation ⋮ A model of PCF in guarded type theory ⋮ Denotational semantics of recursive types in synthetic guarded domain theory ⋮ A Light Modality for Recursion ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Denotational semantics for guarded dependent type theory ⋮ Adjoint reactive GUI programming ⋮ Temporal refinements for guarded recursive types ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Unnamed Item ⋮ A metalanguage for guarded iteration ⋮ Unnamed Item ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Unnamed Item ⋮ Monoidal-closed categories of tree automata ⋮ Modal dependent type theory and dependent right adjoints ⋮ Guarded cubical type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Constructive Modalities with Provability Smack

This page was built for publication: First steps in synthetic guarded domain theory: step-indexing in the topos of trees