Eisbach: a proof method language for Isabelle

DOI10.1007/s10817-015-9360-2zbMath1356.68195OpenAlexW2290529759MaRDI QIDQ287365

Toby Murray, Makarius Wenzel, Daniel Matichuk

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-015-9360-2

zbMATH Keywords

EisbachIsabellel4.verifiedproof automationseL4

Mathematics Subject Classification ID

Related Items

Unnamed Item, Verifying feedforward neural networks for classification in Isabelle/HOL, Parameterized synthesis for fragments of first-order logic over data words, Highly Automated Formal Proofs over Memory Usage of Assembly Code, Unnamed Item, From LCF to Isabelle/HOL, TacticToe: learning to prove with tactics, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant

Uses Software

• Isabelle
• Isabelle/HOL
• LCF
• Coq/SSReflect
• Locales
• Mtac
• Eisbach
• seL4
• Zoo Probabilistic Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Locales: a module system for mathematical theories
• An Isabelle Proof Method Language
• Challenges and Experiences in Managing Large-Scale Proofs
• A Formalized Hierarchy of Probabilistic System Types
• Secure Microkernels, State Monads and Scalable Refinement
• Noninterference for Operating System Kernels
• Mtac
• How to make ad hoc proof automation less ad hoc
• Types for Proofs and Programs