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

Elpi is dialect of λProlog that can be used as an extension language for Coq. It lets one define commands and tactics in a high level programming language tailored to the manipulation of syntax trees containing binders and existentially quantified meta variables.

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
25m
Talk
A “destruct” Tactic for Mtac2
CoqPL
Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET
File Attached
10:55
25m
Talk
Typed Template Coq
CoqPL
Simon Boulier, Matthieu SozeauInria, Nicolas TabareauInria, France, Abhishek AnandCornell University
File Attached
11:20
25m
Talk
Elpi: an extension language for Coq
CoqPL
File Attached
11:45
25m
Talk
Coqatoo: Generating Natural Language Versions of Coq Proofs
CoqPL
Andrew BedfordLaval University
File Attached