Paco: Coq library for Parametric Coinduction
Paco is a Coq library for parametric coinduction. For more information, please see:
- Chung-Kil Hur, Georg Neis, Derek Dreyer and Viktor Vafeiadis. The power of parameterization in coinductive proof. POPL 2013.
- Yannick Zakowski, Paul He, Chung-Kil Hur and Steve Zdancewic. An equational theory for weak bisimulation via generalized parameterized coinduction. CPP 2020.
Paco also supports upto techniques using "companion". See:
- Damien Pous. Coinduction All the Way Up. LICS 2016.
Minki Cho refactored the implementation to speed up the compilation time.
The current version is v4.1.1, and it's compatible with Coq 8.9 - 8.13.
# from opam opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-paco # from source cd src; make; make install # for library files cd src; make doc; make install-doc # for documentation