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

CoqPL-2018
10:30 - 12:10: - Tactics and Proof Engineering at Watercourt A
Chair(s): Benjamin Delaware
CoqPL-2018151583580000010:30 - 10:55
Talk
File Attached
CoqPL-2018151583730000010:55 - 11:20
Talk
File Attached
CoqPL-2018151583880000011:20 - 11:45
Talk
File Attached
CoqPL-2018151584030000011:45 - 12:10
Talk
File Attached