Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant - ERRATUM
No abstract available.
DOI 10.1017/s0956796823000011
Related papers
- Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant JFP 2022
- Automatic induction proofs of data-structures in imperative programs PLDI 2015
- Fold and Unfold for Program Semantics ICFP 1998
- How Powerful are Folding/Unfolding Transformations? JFP 1994
- Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic CPP 2024
- The Tortoise and the Hare Algorithm for Finite Lists, Compositionally TOPLAS 2023
- An unfold/fold transformation framework for definite logic programs TOPLAS 2004
- Equivalence of system f and ź2 in Coq based on context morphism lemmas CPP 2017