Challenges and Experiences in Managing Large-Scale Proofs

DOI10.1007/978-3-642-31374-5_3zbMath1359.68264OpenAlexW1537943690MaRDI QIDQ2907311

Timothy Bourke, Rafal Kolanski, Gerwin Klein, Matthias Daum

Publication date: 7 September 2012

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-31374-5_3

zbMATH Keywords

Isabelle/HOLinteractive theorem provinglarge-scale proof

Mathematics Subject Classification ID

Related Items

Eisbach: a proof method language for Isabelle, Unnamed Item

Uses Software

• Coq
• Isabelle/HOL
• Mizar
• Sledgehammer
• LCF
• seL4
• Archive Formal Proofs