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.

Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change

10:30 - 12:10: Tactics and Proof EngineeringCoqPL at Watercourt A
Chair(s): Benjamin DelawarePurdue University
10:30 - 10:55
Talk
CoqPL
Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET
File Attached
10:55 - 11:20
Talk
CoqPL
Simon Boulier, Matthieu SozeauInria, Nicolas TabareauInria, France, Abhishek AnandCornell University
File Attached
11:20 - 11:45
Talk
CoqPL
File Attached
11:45 - 12:10
Talk
CoqPL
Andrew BedfordLaval University
File Attached