Tool support for proof engineering

DOI10.1016/J.ENTCS.2006.09.023MaRDI QIDQ2867938zbMATH OpenOpenAlexFDO

Authors Anne Mulhern, Ben Liblit, Charles Fischer

Publication date 20 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.1016/j.entcs.2006.09.023

zbMATH Keywords

IDECoqprogram extractionrefactoringprogram visualizationproof strategiesproof dependenciesIPEproof explanationproof frameworkproof reuseproof transformationsproof visualization

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1629953
• scientific article; zbMATH DE number 1629956
• Panoptes: an exploration tool for formal proofs
• ProofViz: an interactive visual proof explorer
• scientific article; zbMATH DE number 2185687

Cites work

• scientific article; zbMATH DE number 1701346 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• A large-scale experiment in executing extracted programs
• Formal proof - the four color theorem
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Synthesis of ML programs in the system Coq
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Towards the animation of proofs -- testing proofs by examples

Cited in

(1)

• scientific article; zbMATH DE number 2024610 (Why is no real title available?)

Describes a project that uses

Uses Software

• BlueJ
• VizzAnalyzer
• CtCoq
• Gammatella
• Isabelle/HOL
• Coq

This page was built for publication: Tool support for proof engineering

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