CITATION.bib

@InProceedings{Alectryon+SLE2020,
  author       = {Pit-Claudel, Clément},
  title        = {Untangling Mechanized Proofs},
  booktitle    = {Proceedings of the 13th {ACM} {SIGPLAN} International
                  Conference on Software Language Engineering},
  year         = 2020,
  series       = {{SLE} 2020},
  pages        = {155–174},
  address      = {New York, NY, USA},
  publisher    = {Association for Computing Machinery},
  isbn         = 9781450381765,
  url          = {https://pit-claudel.fr/clement/papers/alectryon-SLE20.pdf},
  doi          = {10.1145/3426425.3426940},
  abstract     = {Proof assistants like Coq, Lean, or HOL4 rely heavily on
                  stateful meta-programs called scripts to assemble
                  proofs. Unlike pen-and-paper proofs, proof scripts only
                  describe the steps to take (induct on x, apply a theorem, …),
                  not the states that these steps lead to; as a result, plain
                  proof scripts are essentially incomprehensible without the
                  assistance of an interactive user interface able to run the
                  script and show the corresponding proof states. Until now, the
                  standard process to communicate a proof without forcing
                  readers to execute its script was to manually copy-paste
                  intermediate proof states into the script, as source code
                  comments — a tedious and error-prone exercise. Additional
                  prose (such as for a book or tutorial) was likewise embedded
                  in comments, preserving executability at the cost of a
                  mediocre text-editing experience. This paper describes a new
                  approach to the development and dissemination of literate
                  proof scripts, with a focus on the Coq proof
                  assistant. Specifically, we describe two contributions: a
                  compiler that interleaves Coq’s output with the original proof
                  script to produce interactive webpages that are complete,
                  self-contained presentations of Coq proofs; and a new literate
                  programming toolkit that allows authors to switch seamlessly
                  between prose- and code-oriented views of the same sources, by
                  translating back and forth between reStructuredText documents
                  and literate Coq source files. In combination, these tools
                  offer a new way to write, communicate, and preserve proofs,
                  combining the flexibility of procedural proof scripts and the
                  intelligibility of declarative proofs.},
  numpages     = 20,
  keywords     = {formal verification, proof browsing, literate programming,
                  proof presentation},
  location     = {Virtual, USA}
}