Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant

DOI10.1017/S0956796822000107MaRDI QIDQ5051990zbMATH OpenWikidataFDO

Authors Olivier Danvy

Publication date 18 November 2022

Published in Journal of Functional Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Logic Based Program Synthesis and Transformation
• Fold and unfold for program semantics
• Typing total recursive functions in Coq
• scientific article; zbMATH DE number 1670732

Cites work

• scientific article; zbMATH DE number 3907750 (Why is no real title available?)
• scientific article; zbMATH DE number 3502750 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 1503606 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• scientific article; zbMATH DE number 3342643 (Why is no real title available?)
• A Transformation System for Developing Recursive Programs
• A compiled implementation of strong reduction
• Folding left and right over Peano numbers
• Getting There and Back Again
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Lambda-dropping: Transforming recursive equations into programs with block structure
• There and back again

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
• scientific article; zbMATH DE number 1070623 (Why is no real title available?)

Describes a project that uses

Uses Software

• Haskell
• Isabelle/HOL
• Coq

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)