Challenges and experiences in managing large-scale proofs

DOI10.1007/978-3-642-31374-5_3MaRDI QIDQ2907311zbMATH OpenOpenAlexFDO

Authors Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski

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

interactive theorem provingIsabelle/HOLlarge-scale proof

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1746646
• scientific article; zbMATH DE number 1852159
• An Isabelle proof method language
• Challenges of software verification. Contributions of the first workshop, CSV, Venice, Italy, May 20, 2022
• Mining the Archive of Formal Proofs

Cited in

(3)

• Eisbach: a proof method language for Isabelle
• scientific article; zbMATH DE number 7756106 (Why is no real title available?)
• Supporting maintenance of formal mathematics with similarity search

Describes a project that uses

Uses Software

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

This page was built for publication: Challenges and experiences in managing large-scale proofs

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