Tool Support for Proof Engineering

DOI10.1016/j.entcs.2006.09.023zbMath1278.68275OpenAlexW2051323046MaRDI QIDQ2867938

Ben Liblit, Anne Mulhern, Charles N. Fischer

Publication date: 20 December 2013

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

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

zbMATH Keywords

IDEprogram extractionprogram visualizationCoqrefactoringproof strategiesproof dependenciesIPEproof explanationproof frameworkproof reuseproof transformationsproof visualization

Mathematics Subject Classification ID

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Synthesis of ML programs in the system Coq
• Isabelle/HOL. A proof assistant for higher-order logic
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Towards the animation of proofs -- testing proofs by examples

This page was built for publication: Tool Support for Proof Engineering