| Year | 2009 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Grigore Rosu, Dorel Lucanu |
Links
Abstract
Several algorithmic variants of circular coinduction have been proposed and implemented during the last decade, but a proof theoretical foundation of circular coinduction in its full generality is still missing.
This paper gives a three-rule proof system that can be used to formally derive circular coinductive proofs. This three-rule system is proved behaviorally sound and is exemplied by proving several properties of infinite streams. Algorithmic variants of circular coinduction now become heuristics to search for proof derivations using the three rules.
BibTeX
@inproceedings{rosu-lucanu-2009-calco,
author = {Grigore Roc{s}u and Dorel Lucanu},
title = {Circular Coinduction -- A Proof Theoretical Foundation},
booktitle = {CALCO 2009},
year = {2009},
series = {LNCS},
booktitle = {CALCO 2009},
volume = {5728},
pages = {127--144},
publisher = {Springer},
url_publisher = {http://www.springer.com/?SGWID=0-102-24-0-0&searchType=EASY_CDA&queryText=5728},
url = {http://calco09.dimi.uniud.it/[CALCO]}
}