POPL 2018
Sun 7 - Sat 13 January 2018 Los Angeles, California, United States
POPL 2018 (series) / CoqPL 2018 (series) / The Fourth International Workshop on Coq for Programming Languages /

Coqatoo: Generating Natural Language Versions of Coq Proofs

CoqPL 2018
Sat 13 Jan 2018 11:45 - 12:10 at Watercourt A - Tactics and Proof Engineering Chair(s): Benjamin Delaware

We present Coqatoo, a command-line utility capable of automatically generating natural language versions of Coq proofs. We illustrate its use on a simple proof.

(Bedford-CoqPL18.pdf)687KiB
(Bedford-CoqPL18-Slides.pdf)327KiB

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
Tactics and Proof EngineeringCoqPL at Watercourt A
Chair(s): Benjamin Delaware Purdue University
10:30
25m
Talk
A “destruct” Tactic for Mtac2
CoqPL
Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET
File Attached
10:55
25m
Talk
Typed Template Coq
CoqPL
Simon Boulier , Matthieu Sozeau Inria, Nicolas Tabareau Inria, France, Abhishek Anand Cornell University
File Attached
11:20
25m
Talk
Elpi: an extension language for Coq
CoqPL
Enrico Tassi INRIA
File Attached
11:45
25m
Talk
Coqatoo: Generating Natural Language Versions of Coq Proofs
CoqPL
Andrew Bedford Laval University
File Attached
Andrew Bedford

Andrew Bedford

Laval University