Skip to main content


eCommons@Cornell

eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/30510
Title: Practical Coinduction
Authors: Kozen, Dexter
Silva, Alexandra
Keywords: coinduction
coalgebra
verification
Issue Date: 11-Nov-2012
Abstract: Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively-defined datatypes such as finite lists, finite trees, and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes.
URI: http://hdl.handle.net/1813/30510
Appears in Collections:Computing and Information Science Technical Reports

Files in This Item:

File Description SizeFormat
Structural.pdfMain article211.76 kBAdobe PDFView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us