Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant
From MaRDI portal
Publication:5051990
DOI10.1017/S0956796822000107WikidataQ124817274 ScholiaQ124817274MaRDI QIDQ5051990FDOQ5051990
Authors: Olivier Danvy 
Publication date: 18 November 2022
Published in: Journal of Functional Programming (Search for Journal in Brave)
Recommendations
Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Transformation System for Developing Recursive Programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A compiled implementation of strong reduction
- There and back again
- Lambda-dropping: Transforming recursive equations into programs with block structure
- Getting There and Back Again
- Folding left and right over Peano numbers
Cited In (5)
- On Inductive and Coinductive Proofs via Unfold/Fold Transformations
- Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant – ERRATUM
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- Title not available (Why is that?)
Uses Software
This page was built for publication: Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5051990)
