5 search results for "tag:"keyword:coinduction""

Showing 1 - 5

coq-coinduction-examples

No documentation

Examples on how to use the coq-coinduction library, for doing proofs by (enhanced) coinduction

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

Damien Pous

1.7

LGPL-3.0-or-later

Used by 0 other packages

13 Jul 2023
coq-ctree

No documentation

Library for representing recursive, non-deterministic and impure programs with equational reasoning

category:CS/Semantics and Compilation/Semantics category:CS/Concurrency/Theory of concurrent systems keyword:simulation keyword:bisimilarity keyword:coinduction up-to keyword:process algebra keyword:cooperative multithreading logpath:CTree

Nicolas Chappe Paul He Ludovic Henrio Yannick Zakowski Steve Zdancewic

2.0

MIT

Used by 1 other packages

29 Jul 2025
coq-freesim

No documentation

Stuttering For Free

keyword:simulation keyword:coinduction keyword:dual non-determinism keyword:up to techniques keyword:companion keyword:Interaction Trees keyword:CompCert logpath:FreeSim

Minki Cho, Youngju Song, Dongjae Lee

1.0.0

BSD-3-Clause

Used by 0 other packages

19 Sep 2023
rocq-coinduction

No documentation

A library for doing proofs by (enhanced) coinduction

keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity logpath:Coinduction date:2025-09-17

Damien Pous <Damien.Pous@ens-lyon.fr>

1.21

LGPL-3.0-or-later

Used by 1 other packages

19 Sep 2025
rocq-sims

No documentation

A library of various strong and weak simulation relations

category:Computer Science/Semantics and Compilation/Semantics category:Computer Science/Semantics and Compilation/Compilation keyword:simulation keyword:coinduction up-to logpath:Sims

Nicolas Chappe

0.2

LGPL-3.0-or-later

Used by 0 other packages

27 Nov 2025