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

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