@InProceedings{HausmannEtAl05,
  author = {Daniel Hausmann and Till Mossakowski and Lutz Schr{\"o}der},
  title = {Iterative Circular Coinduction for {CoCASL} in {Isabelle/HOL}},
  year = {2005},
  editor = {Maura Cerioli},
  booktitle = {Fundamental Approaches to Software Engineering 2005},
  publisher = {Springer; Berlin; http://www.springer.de},
  series = {Lecture Notes in Computer Science},
  volume = {3442},
  pages = {341-356},
  keywords = {circular coinduction coalgebra CoCASL Isabelle},
  url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3442&spage=341},
  comment = { <a href = "http://www.informatik.uni-bremen.de/~till/papers/coinduction.pdf"> [preprint] </a>},
  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 emph{circular
coinduction} allows a higher degree of automation. As part of an effort
to provide proof support for the algebraic-coalgebraic specification
language textmd{textsc{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 of textmd{textsc{CoCasl}}
specifications, automatically translated into Isabelle theories by means
of the Bremen heterogeneous CASL tool set Hets.},
}