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

Full work available at URL https://doi.org/10.1017/S0956796822000107

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

• A compiled implementation of strong reduction
• A Transformation System for Developing Recursive Programs
• Folding left and right over Peano numbers
• Getting There and Back Again
• 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?)
• 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)

• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• On Inductive and Coinductive Proofs via Unfold/Fold Transformations
• scientific article; zbMATH DE number 1070623 (Why is no real title available?)
• Deep Generation of Coq Lemma Names Using Elaborated Terms
• Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant – ERRATUM

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Haskell

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)