An Isabelle proof method language

DOI10.1007/978-3-319-08970-6_25MaRDI QIDQ2879265zbMATH OpenOpenAlexFDO

Authors Daniel Matichuk, Makarius Wenzel, Toby Murray

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08970-6_25

Mathematics Subject Classification ID

Recommendations

• Eisbach: a proof method language for Isabelle
• A comparison of Mizar and Isar
• Automatic proof and disproof in Isabelle/HOL
• Semi-intelligible Isar proofs from machine-generated proofs
• The Isabelle Framework

Cited in

(8)

• Eisbach
• Eisbach: a proof method language for Isabelle
• Challenges and experiences in managing large-scale proofs
• A formalized hierarchy of probabilistic system types. Proof pearl
• ProofScript: proof scripting for the masses
• The Isabelle Framework
• Formalization quality in Isabelle
• SSCalc: a calculus for Solidity smart contracts

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/Isar

This page was built for publication: An Isabelle proof method language

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