Temporal refinements for guarded recursive types
From MaRDI portal
Publication:2233479
DOI10.1007/978-3-030-72019-3_20zbMath1473.68047OpenAlexW3043298057MaRDI QIDQ2233479
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-72019-3_20
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)
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