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.5.tar.gz
sha512=ac0a4fd9e2a2e0a3477137b35543c5a6043521bb0ea7e030630ddaafc28451554b2d5d927627e10dc539f1f623ebc8c7779f69bc45a1f99fb5e05ee6581609dc

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: 30 Mar 2022

Dev Dependencies

None

Used by

None

Conflicts

None