Structured formal development in Isabelle

MaRDI QIDQ3431400zbMATH OpenFDO

Authors Maksym Bortin, Einar Broch Johnsen, Christoph Lüth

Publication date 10 April 2007

zbMATH Keywords

program developmenttheorem provers

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• An approach to the extension of a theorem prover by advanced structuring mechanisms.
• Structured formal development with quotient types in Isabelle/HOL
• The Isabelle Framework
• scientific article; zbMATH DE number 1088221
• The foundation of a generic theorem prover

Cited in

(11)

• Synthesis of implementations for divide-and-conquer specifications
• Aligning concepts across proof assistant libraries
• Structured formal development with quotient types in Isabelle/HOL
• The Isabelle Framework
• Matching concepts across HOL libraries
• Towards logical frameworks in the heterogeneous tool set Hets
• Local Theory Specifications in Isabelle/Isar
• An approach to the extension of a theorem prover by advanced structuring mechanisms.
• Formalising Generalised Substitutions
• Generic tools via general refinement
• scientific article; zbMATH DE number 2003150 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle/Isar
• TkWinHOL
• Isabelle

This page was built for publication: Structured formal development in Isabelle

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