scientific article; zbMATH DE number 2185691

zbMATH Open1063.03501MaRDI QIDQ3024873FDOQ3024873

Authors:

Publication date: 4 July 2005

Title of this publication is not available (Why is that?)

Recommendations

• Publication:4945200
• 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

Mathematics Subject Classification ID

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

Cited In (11)

• A fixedpoint approach to implementing (co)inductive definitions
• A proof tool for reasoning about functional programs
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Title not available (Why is that?)
• On definitions of constants and types in HOL
• Title not available (Why is that?)
• Bounded Relational Analysis of Free Data Types
• Set theory for verification. II: Induction and recursion
• Automated flaw detection in algebraic specifications
• Title not available (Why is that?)
• Friends with benefits. Implementing corecursion in foundational proof assistants

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)