Structured formal development with quotient types in Isabelle/HOL

DOI10.1007/978-3-642-14128-7_5MaRDI QIDQ3582695zbMATH OpenOpenAlexFDO

Authors Maksym Bortin, Christoph Lüth

Publication date 24 August 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14128-7_5

Mathematics Subject Classification ID

Recommendations

• Structured formal development in Isabelle
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• An approach to the extension of a theorem prover by advanced structuring mechanisms.
• Theorem Proving in Higher Order Logics
• Publication:4944854

Cited in

(5)

• JEFL: joint embedding of formal proof libraries
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• An approach to the extension of a theorem prover by advanced structuring mechanisms.
• Structured formal development in Isabelle
• scientific article; zbMATH DE number 7649960 (Why is no real title available?)

Describes a project that uses

Uses Software

• MAYA
• Isabelle/HOL
• Isabelle

This page was built for publication: Structured formal development with quotient types in Isabelle/HOL

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