Formalization quality in Isabelle

DOI10.1007/978-3-031-42753-4_10MaRDI QIDQ6118825zbMATH OpenOpenAlexFDO

Authors Fabian Huch, Yiannos Stathopoulos

Publication date 28 February 2024

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

Full work available at URL https://doi.org/10.1007/978-3-031-42753-4_10

zbMATH Keywords

change frequencycode smelldeep learningformalization qualityIsabellelintermachine learningstatic analysis

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Recommendations

• Formal entity graphs as complex networks: assessing centrality metrics of the archive of formal proofs
• Simple dataset for proof method recommendation in Isabelle/HOL
• Recycling proof patterns in Coq: case studies
• An Isabelle proof method language
• Mining the Archive of Formal Proofs

Cites work

• Formal entity graphs as complex networks: assessing centrality metrics of the archive of formal proofs

Cited in

(1)

• Supporting maintenance of formal mathematics with similarity search

This page was built for publication: Formalization quality in Isabelle

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