Sat 13 Jan 2018 10:30 - 10:55 at Watercourt A - Tactics and Proof Engineering Chair(s): Benjamin Delaware

We present a “destruct” tactic that supports dependent types written in Mtac2. The tactic is implemented to a large degree in Coq itself — only using Mtac2’s unsafe features when absolutely necessary. To this end, the development includes fully-typed descriptions of 1) inductive datatypes, 2) arguments of inductive datatypes, 3) constructors of inductive dataypes, 4) branches of matches on values of inductive datatypes, and 5) return types of matches on values of inductive datatypes. Additionally, we also propose a way of dealing with meta-programs that are parametric in Prop/Type.

Kaiser-Ziliani-CoqPL18.pdf (Kaiser-Ziliani-CoqPL18.pdf)532KiB

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