Circular coinduction: a proof theoretical foundation
From MaRDI portal
Publication:2888482
Recommendations
Cites work
- scientific article; zbMATH DE number 3970817 (Why is no real title available?)
- scientific article; zbMATH DE number 1740032 (Why is no real title available?)
- 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
Cited in
(36)- Final semantics for decorated traces
- Foundations for structuring behavioural specifications
- CIRC: A Behavioral Verification Tool Based on Circular Coinduction
- CafeOBJ Traces
- Shall we juggle, coinductively?
- CIRC: A Circular Coinductive Prover
- A Decision Procedure for Bisimilarity of Generalized Regular Expressions
- Coinduction in Flow: The Later Modality in Fibrations
- Behavioral equivalence of hidden k-logics: an abstract algebraic approach
- Behavioral rewrite systems and behavioral productivity
- Matching logic explained
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- Loop verification with invariants and contracts
- Soundness and completeness proofs by coinductive methods
- Proof-theoretic foundations of normal logic programs
- Non-well-founded deduction for induction and coinduction
- Integrating induction and coinduction via closure operators and proof cycles
- Behavioral and coinductive rewriting
- Coalgebras in functional programming and type theory
- Conditional circular coinductive rewriting with case analysis.
- Cyclic implicit complexity
- Addressing Circular Definitions via Systems of Proofs
- Program equivalence by circular reasoning
- A generic framework for symbolic execution: a coinductive approach
- Algebra and Coalgebra in Computer Science
- Fundamental Approaches to Software Engineering
- Circular coinduction in Coq using bisimulation-up-to techniques
- Circular (yet sound) proofs
- Practical coinduction
- Coinduction in uniform: foundations for corecursive proof search with Horn clauses
- Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
- Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
- scientific article; zbMATH DE number 2087442 (Why is no real title available?)
- Bisimulations generated from corecursive equations
- Regular strategies as proof tactics for \textsf{CIRC}
- Sound and complete equational reasoning over comodels
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)
