scientific article; zbMATH DE number 1424015

MaRDI QIDQ4945204zbMATH OpenFDO

Authors

Publication date 20 September 2000

zbMATH Keywords

contracting functionconverging equivalence relationIsabelle theorem proverrecursive functionsunique fixed pointwell-founded recursion

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Recursive functions and relations, subrecursive hierarchies (03D20)

Recommendations

• A fixedpoint approach to implementing (co)inductive definitions
• Mechanizing coinduction and corecursion in higher-order logic
• scientific article; zbMATH DE number 2003155
• General Recursion via Coinductive Types
• Recursive Functions on Lazy Lists via Domains and Topologies

Cited in

(10)

• Adapting functional programs to higher order logic
• A term calculus for (co-)recursive definitions on streamlike data structures
• Inductive and coinductive components of corecursive functions in Coq
• scientific article; zbMATH DE number 3980461 (Why is no real title available?)
• Mechanizing coinduction and corecursion in higher-order logic
• A fixedpoint approach to implementing (co)inductive definitions
• General Recursion via Coinductive Types
• Primitive recursive functional with dependent types
• Formal definitions and proofs for partial (co)recursive functions
• Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching

Describes a project that uses

Uses Software

• Coq
• Isabelle

This page was built for publication:

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