Write a Blog >>
SLE 2020
Sun 15 - Fri 20 November 2020 Online Conference
co-located with SPLASH 2020
Mon 16 Nov 2020 15:20 - 15:40 at SPLASH-III - Chair(s): Paddy Krishnan
Tue 17 Nov 2020 03:20 - 03:40 at SPLASH-III - Chair(s): Ralf Lämmel

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.

I’m a PhD candidate at MIT, working in Adam Chlipala’s lab. My research focuses on proof assistants, extensible compilers, and programming languages; my broader interests include hardware design languages, optimization, databases, and type theory. I work on end-to-end verified compilation pipelines from high-level specifications to assembly language, verified compilers and fast simulation for rule-based hardware design languages with EHRs, and Coq tooling.
And I’m applying for faculty positions this year!

Mon 16 Nov
Times are displayed in time zone: Central Time (US & Canada) change

15:00 - 15:40: SLE at SPLASH-III +12h
Chair(s): Paddy KrishnanOracle Labs, Australia
15:00 - 15:20
Talk
SLE
Sergio Queiroz de MedeirosUniversidade Federal do Rio Grande do Norte, Carlos OlarteFederal University of Rio Grande do Norte, Brazil
Link to publication DOI Pre-print Media Attached
15:20 - 15:40
Talk
SLE
DOI Pre-print Media Attached

Tue 17 Nov
Times are displayed in time zone: Central Time (US & Canada) change

03:00 - 03:40: SLE at SPLASH-III
Chair(s): Ralf LämmelFacebook London
03:00 - 03:20
Talk
SLE
Sergio Queiroz de MedeirosUniversidade Federal do Rio Grande do Norte, Carlos OlarteFederal University of Rio Grande do Norte, Brazil
Link to publication DOI Pre-print Media Attached
03:20 - 03:40
Talk
SLE
DOI Pre-print Media Attached