Untangling Mechanized Proofs
summary
Alectryon is a Python toolkit that runs Coq on source files, captures tactic outputs and goals, and emits interactive web visualizations that inline inputs and Coq’s recorded outputs so proofs are explorable without running Coq. It also provides a bidirectional translator between Coq sources and reStructuredText, preserving cursor positions. The implementation compiles tens of thousands of lines (including Coq’s stdlib and a Software Foundations volume), is used in the wild, and shows a median overhead of 3x compilation time.
AI-written summary · about
chapters (5)
related talks
46mMechanizing Abstract Interpretation
01h 34mFormal Logic Undressed
31mA Coq Library of Undecidable Problems
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
21mCompositional pre-processing for automated reasoning in dependent type theory
27mAn Equations Tutorial
42mMetaCoq as a tool to prevent future unsoundness in Coq