Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants
No abstract available.
Related papers
- Foundational extensible corecursion: a proof assistant perspective ICFP 2015
- Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses ESOP 2019
- Defining Corecursive Functions in Coq Using Approximations ECOOP 2022
- Coco: Corecursion with Compositional Heterogeneous Productivity POPL 2026
- Classical (co)recursion: Mechanics JFP 2023
- Sound Regular Corecursion in coFJ ECOOP 2020
- Lambda, the ultimate TA: using a proof assistant to teach programming language foundations ICFP 2009
- Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean CAV 2026