Weak Bisimulation via Generalized Parameterized Coinduction
summary
Claims a gPaco generalization of the Paco coinduction library that adds a second parameter to fix an information‑leak in parameterized coinduction, implemented in Coq Paco library and available on GitHub. Demonstrates on finite/infinite streams with visible and tau steps (proving s0 ~ t0, s1 ~ t1) that the two‑parameter scheme preserves incremental proof construction, yields sound up‑to and directed‑rewriting principles, and remains backward compatible with existing Paco proofs. The implementation works and recovers stronger, more precise coinductive proof rules.
AI-written summary · about
chapters (11)
- 0:00Weak Bisimulation via Generalized Parameterized Coinduction
- 0:56Coinductive Lists of Naturals
- 4:14A Minimal Example
- 8:05Extending Paco with a Second Parameter
- 9:35Generalized Paco
- 10:26Rewriting eutt-Equations
- 11:49A Parameterized Weak Bisimulation
- 13:07Soundness
- 13:28Knowledge Manipulation
- 13:53Stream Processing
- 15:28Conclusion
related talks
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
15mCompiling with Continuations, Correctly
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
19mExtensible Metatheory Mechanization via Family Polymorphism
30mPlausible sealing for gradual parametricity