The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

*************************************************************************
        Paco: A Coq Library for Parameterized Coinduction
*************************************************************************

We are pleased to announce the first release of Paco, a Coq library
implementing parameterized coinduction.  Parameterized coinduction is
a technique for defining coinductive predicates (i.e., in Prop), using
which one can perform coinductive proofs in a more compositional and
incremental fashion than with standard Tarski-style constructions.

The Paco library provides a tactic called "pcofix", replacing Coq's
primitive cofix and avoiding its syntactic guardedness checking of
proof terms.  We have found that pcofix yields clear performance and
usability benefits, even on simple examples.

The library is compatible with both Coq 8.3 and 8.4.  It is available,
along with a tutorial and a draft paper on parameterized coinduction,
at the following URL:

        http://plv.mpi-sws.org/paco/

Best regards,
Chung-Kil Hur, Georg Neis, Derek Dreyer and Viktor Vafeiadis