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.7.tar.gz
sha512=229b7d82fae725875c8a9acc099dee8a7fb24e14620d2b9d6bb48da9727312cadb93d8defe58fcee87d1af5f0548258eab0c9bfd03e4c0ce68aed9063e513d27

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