Circular Coinduction: A Proof Theoretical Foundation

DOI10.1007/978-3-642-03741-2_10zbMath1239.68067OpenAlexW1498001169MaRDI QIDQ2888482

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

Mathematics Subject Classification ID

Structure of proofs (03F07) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (20)

CIRC: A Behavioral Verification Tool Based on Circular Coinduction ⋮ Behavioral equivalence of hidden \(k\)-logics: an abstract algebraic approach ⋮ Bisimulations Generated from Corecursive Equations ⋮ Final Semantics for Decorated Traces ⋮ Loop verification with invariants and contracts ⋮ Foundations for structuring behavioural specifications ⋮ Proof-theoretic foundations of normal logic programs ⋮ Practical coinduction ⋮ Coalgebras in functional programming and type theory ⋮ Sound and complete equational reasoning over comodels ⋮ A Decision Procedure for Bisimilarity of Generalized Regular Expressions ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Program equivalence by circular reasoning ⋮ CafeOBJ Traces ⋮ Behavioral Rewrite Systems and Behavioral Productivity ⋮ Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ Matching logic explained ⋮ Non-well-founded deduction for induction and coinduction ⋮ Integrating induction and coinduction via closure operators and proof cycles

Uses Software

• Isabelle/HOL
• CIRC
• Maude
• CoCasl

Cites Work

• Unnamed Item
• Unnamed Item
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• Constructor-based observational logic
• CIRC: A Behavioral Verification Tool Based on Circular Coinduction
• CIRC: A Circular Coinductive Prover
• Fundamental Approaches to Software Engineering
• Recent Trends in Algebraic Development Techniques

This page was built for publication: Circular Coinduction: A Proof Theoretical Foundation