A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction
No abstract available.
Related papers
- A Rose Tree Is Blooming (Proof Pearl) CPP 2026
- Generalizing Inference Systems by Coaxioms ESOP 2017
- A nominal exploration of intuitionism CPP 2016
- Bar Inductive Predicates for Constructive Algebra in Rocq CPP 2026
- Coinduction inductively: mechanizing coinductive proofs in Liquid Haskell Haskell 2022
- Mixed Inductive/Coinductive Types and Strong Normalization APLAS 2007
- Copatterns: programming infinite structures by observations POPL 2013
- Rely-Guarantee Is Coinductive - - A Proof-Centered Investigation of Inductively Approximated Coinduction - ESOP 2026