Circular coinduction: a proof theoretical foundation
From MaRDI portal
Recommendations
Cites work
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- CIRC: A Behavioral Verification Tool Based on Circular Coinduction
- CIRC: A Circular Coinductive Prover
- Conditional circular coinductive rewriting with case analysis.
- Constructor-based observational logic
- Context induction: A proof principle for behavioural abstractions and algebraic implementations
- Fundamental Approaches to Software Engineering
- scientific article; zbMATH DE number 3970817 (Why is no real title available?)
- scientific article; zbMATH DE number 1740032 (Why is no real title available?)
Cited in
(40)- Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- Matching logic explained
- Non-well-founded deduction for induction and coinduction
- Integrating induction and coinduction via closure operators and proof cycles
- Loop verification with invariants and contracts
- Circular (yet sound) proofs
- Soundness and completeness proofs by coinductive methods
- Behavioral and coinductive rewriting
- Regular strategies as proof tactics for \textsf{CIRC}
- CIRC: A Behavioral Verification Tool Based on Circular Coinduction
- A Decision Procedure for Bisimilarity of Generalized Regular Expressions
- Behavioral equivalence of hidden k-logics: an abstract algebraic approach
- Bisimulations generated from corecursive equations
- Final semantics for decorated traces
- Addressing Circular Definitions via Systems of Proofs
- CIRC: A Circular Coinductive Prover
- Foundations for structuring behavioural specifications
- scientific article; zbMATH DE number 1330138 (Why is no real title available?)
- scientific article; zbMATH DE number 2087442 (Why is no real title available?)
- Shall we juggle, coinductively?
- Program equivalence by circular reasoning
- Foundations of regular coinduction
- A generic framework for symbolic execution: a coinductive approach
- Fundamental Approaches to Software Engineering
- Circular coinduction in Coq using bisimulation-up-to techniques
- Practical coinduction
- CafeOBJ Traces
- Behavioral rewrite systems and behavioral productivity
- Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
- Algebra and Coalgebra in Computer Science
- Coinduction in Flow: The Later Modality in Fibrations
- Conditional circular coinductive rewriting with case analysis.
- Sound and complete equational reasoning over comodels
- Coinduction in uniform: foundations for corecursive proof search with Horn clauses
- Proof-theoretic foundations of normal logic programs
- Coalgebras in functional programming and type theory
- Cyclic implicit complexity
- Checking equivalence in a non-strict language
- Cartesian reachability logic: a language-parametric logic for verifying k-safety properties
This page was built for publication: Circular coinduction: a proof theoretical foundation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2888482)
