SRI PVS:Community Portal

From SRI PVS

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.