| Publication type: |
Article in Proceedings |
| Author: |
Daniel Hausmann, Till Mossakowski, Lutz Schröder |
| Editor: |
Maura Cerioli |
| Title: |
Iterative Circular Coinduction for CoCASL in Isabelle/HOL |
| Book / Collection title: |
Fundamental Approaches to Software Engineering 2005 |
| Volume: |
3442 |
| Page(s): |
341 – 356 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2005 |
| Publisher: |
Springer, Berlin |
| 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 emphcircular
coinduction allows a higher degree of automation. As part of an effort
to provide proof support for the algebraic-coalgebraic specification
language textmdtextscCoCasl, 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 of textmdtextscCoCasl
specifications, automatically translated into Isabelle theories by means
of the Bremen heterogeneous CASL tool set Hets. |
| Internet: |
http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3442&spage=341 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~till/papers/coinduction.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~till/papers/coinduction.ps |
| Keywords: |
circular coinduction coalgebra CoCASL Isabelle |
| Status: |
Reviewed |
| Last updated: |
22. 06. 2005 |
