coq-coalgebras

Coalgebras, bisimulation and lambda-coiteration. This contribution contains a formalisation of coalgebras, bisimulation on coalgebras, weakly final coalgebras, lambda-coiteration definition scheme (including primitive corecursion) and a version of lambda-bisimulation. The formalisation is modular. The implementation of the module types for streams and potentially infinite Peano numbers are provided using the coinductive types.

opam install coq-coalgebras.8.5.0
homepage
https://github.com/coq-contribs/coalgebras
license
LGPL
bugs tracker
https://github.com/coq-contribs/coalgebras/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/coalgebras/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-coalgebras/coq-coalgebras.8.5.0