package coq-coinduction-examples

  1. Overview
  2. No Docs
Examples on how to use the coq-coinduction library, for doing proofs by (enhanced) coinduction

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. D
    Damien Pous

Maintainers

  1. D
    damien.pous@ens-lyon.fr

Sources

v1.6.tar.gz
sha512=ba6847950c729f6d2ba911fadeb0dbcd398aeadee3b69002f3bb59fcc52cc8a5f2f3fc275350d43c0712206a9a1ed7709849b40dc9dca3861c346c809115e94c

Description

Coinductive predicates are greatest fixpoints of monotone functions. The `companion' makes it possible to enhance the associated coinduction scheme. The coq-coinduction library provides tools to exploit such techniques; the present library illustrates its usage on three examples: divergence, Milner's CCS, and Rutten's stream calculus.

Tags

keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity keyword:divergence keyword:streams keyword:CCS logpath:CoinductionExamples

Published: 13 Jul 2023

Dev Dependencies

None

Used by

None

Conflicts

None