@inproceedings{HausmannEtAl05,
  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.},
  added-at = {2016-08-05T15:59:03.000+0200},
  author = {Hausmann, Daniel and Mossakowski, Till and Schr{\"o}der, Lutz},
  biburl = {https://www.bibsonomy.org/bibtex/28ebca3cd8e4c7ddd793b677ec51281cb/tillmo},
  booktitle = {Fundamental Approaches to Software Engineering 2005},
  editor = {Cerioli, Maura},
  interhash = {f1841b48e1fdd376b42fe78bfd76115b},
  intrahash = {8ebca3cd8e4c7ddd793b677ec51281cb},
  keywords = {CoCASL Isabelle circular coalgebra coinduction},
  pages = {341-356},
  pdfurl = {http://www.informatik.uni-bremen.de/~till/papers/coinduction.pdf},
  psurl = {http://www.informatik.uni-bremen.de/~till/papers/coinduction.ps},
  publisher = {Springer; Berlin; http://www.springer.de},
  series = {Lecture Notes in Computer Science},
  status = {Reviewed},
  timestamp = {2016-08-05T15:59:03.000+0200},
  title = {Iterative Circular Coinduction for {CoCASL} in {Isabelle/HOL}},
  url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3442&spage=341},
  volume = 3442,
  year = 2005
}