SRI PVS:Community Portal

From SRI PVS

Revision as of 02:11, 4 February 2007; Leepike (Talk | contribs)
(diff) ←Older revision | Current revision | Newer revision→ (diff)
Jump to: navigation, search
[edit]

Coinduction in PVS

(Posted by Lee Pike <leepike at galois.com>.)

Here's a simple example of coinductive definitions and coinductive reasoning in PVS: coinduction.dmp. For a more complete tutorial, I enjoyed Bart Jacob and Jan Rutten's A tutorial on (co)algebras and (co)induction.

Retrieved from "http://pvs-wiki.csl.sri.com/index.php/SRI_PVS:Community_Portal"
Personal tools