scientific article; zbMATH DE number 2185691

MaRDI QIDQ3024873zbMATH OpenFDO

Authors

Publication date 4 July 2005

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Inductive definability (03D70)

Recommendations

• scientific article; zbMATH DE number 1424012
• Mechanizing coinduction and corecursion in higher-order logic
• Set theory for verification. II: Induction and recursion
• A fixedpoint approach to implementing (co)inductive definitions
• scientific article; zbMATH DE number 1614686

Cited in

(12)

• Set theory for verification. II: Induction and recursion
• scientific article; zbMATH DE number 1614686 (Why is no real title available?)
• On definitions of constants and types in HOL
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Automating Algebraic Specifications of Non-freely Generated Data Types
• scientific article; zbMATH DE number 3938531 (Why is no real title available?)
• scientific article; zbMATH DE number 1424012 (Why is no real title available?)
• A fixedpoint approach to implementing (co)inductive definitions
• Bounded Relational Analysis of Free Data Types
• Automated flaw detection in algebraic specifications
• A proof tool for reasoning about functional programs
• Inductive predicates via least fixpoints in higher-order separation logic

Describes a project that uses

Uses Software

• HOL

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 Q3024873)