Sciweavers

Share
FASE
2005
Springer

Iterative Circular Coinduction for CoCasl in Isabelle/HOL

10 years 9 months ago
Iterative Circular Coinduction for CoCasl in Isabelle/HOL
Abstract. Coalgebra has in recent years been recognized as the framework of choice for the treatment of reactive systems at an appropriate level of generality. Proofs about the reactive behavior of a coalgebraic system typically rely on the method of coinduction. In comparison to ‘traditional’ coinduction, which has the disadvantage of requiring the invention of a bisimulation relation, the method of circular coinduction allows a higher degree of automation. As part of an effort to provide proof support for the algebraic-coalgebraic specification language CoCasl, we develop a new coinductive proof strategy which iteratively constructs a bisimulation relation, thus arriving at a new variant of circular coinduction. Based on this result, we design and implement tactics for the theorem prover Isabelle which allow for both automatic and semiautomatic coinductive proofs. The flexibility of this approach is demonstrated by means of examples of (semi-)automatic proofs of consequences o...
Daniel Hausmann, Till Mossakowski, Lutz Schrö
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FASE
Authors Daniel Hausmann, Till Mossakowski, Lutz Schröder
Comments (0)
books