Temporal refinements for guarded recursive types

DOI10.1007/978-3-030-72019-3_20zbMath1473.68047OpenAlexW3043298057MaRDI QIDQ2233479

Guilhem Jaber, Colin Riba

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-72019-3_20

zbMATH Keywords

refinement types\( \mu \)-calculuscoinductive typesguarded recursive typestopos of trees

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Temporal refinements for guarded recursive types

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The coinductive resumption monad
• Completeness for flat modal fixpoint logics
• Results on the propositional \(\mu\)-calculus
• Sheaves in geometry and logic: a first introduction to topos theory
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Temporal refinements for guarded recursive types
• Guarded cubical type theory
• Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study
• Guarded Dependent Type Theory with Coinductive Types
• Refinement types for Haskell
• Temporal verification of higher-order functional programs
• Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• The mu-calculus and Model Checking
• A very modal model of a modern, major, general type system
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Abstract interpretation from Büchi automata
• Local temporal reasoning
• A type theory for productive coprogramming via guarded recursion
• Martin Hofmann's Case for Non-Strictly Positive Data Types
• Denotational semantics for guarded dependent type theory
• A Generalized Modality for Recursion
• A Fixpoint Logic and Dependent Effects for Temporal Property Verification
• Multimodal Dependent Type Theory
• Fold/Unfold Transformations for Fixpoint Logic
• Modal dependent type theory and dependent right adjoints
• Productive coprogramming with guarded recursion
• Higher-order functional reactive programming without spacetime leaks
• A relational modal logic for higher-order stateful ADTs
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Functional reactive animation
• Well-founded recursion with copatterns and sized types
• Fair reactive programming
• Automatic Termination Verification for Higher-Order Functional Programs
• Applicative programming with effects
• Types and trace effects of higher order programs
• Programming Languages and Systems

This page was built for publication: Temporal refinements for guarded recursive types