Circular coinduction: a proof theoretical foundation
From MaRDI portal
Publication:2888482
DOI10.1007/978-3-642-03741-2_10zbMATH Open1239.68067OpenAlexW1498001169MaRDI QIDQ2888482FDOQ2888482
Authors: Dorel Lucanu, Grigore Roşu 
Publication date: 1 June 2012
Published in: Algebra and Coalgebra in Computer Science (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/2142/10840
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Structure of proofs (03F07)
Cites Work
- CIRC: A Behavioral Verification Tool Based on Circular Coinduction
- CIRC: A Circular Coinductive Prover
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Title not available (Why is that?)
- Conditional circular coinductive rewriting with case analysis.
- Title not available (Why is that?)
- 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
- Coinduction in Flow: The Later Modality in Fibrations
- A Decision Procedure for Bisimilarity of Generalized Regular Expressions
- 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
- Proof-theoretic foundations of normal logic programs
- Loop verification with invariants and contracts
- Soundness and completeness proofs by coinductive methods
- 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
- Cyclic implicit complexity
- Conditional circular coinductive rewriting with case analysis.
- Addressing Circular Definitions via Systems of Proofs
- Algebra and Coalgebra in Computer Science
- Program equivalence by circular reasoning
- Fundamental Approaches to Software Engineering
- A generic framework for symbolic execution: a coinductive approach
- Circular coinduction in Coq using bisimulation-up-to techniques
- Practical coinduction
- Coinduction in uniform: foundations for corecursive proof search with Horn clauses
- Circular (yet sound) proofs
- 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
- Title not available (Why is that?)
- Bisimulations generated from corecursive equations
- Sound and complete equational reasoning over comodels
- Regular strategies as proof tactics for \textsf{CIRC}
Uses Software
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)
