The optimal fixed point combinator

DOI10.1007/978-3-642-14052-5_15MaRDI QIDQ5747650zbMATH OpenOpenAlexFDO

Authors Arthur Charguéraud

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_15

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• Foundations of Software Science and Computation Structures
• Mechanizing coinduction and corecursion in higher-order logic
• Admissibility of cut in LC with fixed point combinator
• scientific article; zbMATH DE number 2003155
• A fixedpoint approach to implementing (co)inductive definitions

Cited in

(4)

• Balancing weight-balanced trees
• Formal definitions and proofs for partial (co)recursive functions
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• scientific article; zbMATH DE number 7226002 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: The optimal fixed point combinator

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747650)