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

Template-Coq is a plugin for Coq, originally implemented by Malecha, which provides a reifier for Coq terms and global declarations, as represented in the Coq kernel, as well as a denotation command. Initially, it was developed for the purpose of writing simple functions on Coq ’s AST. Recently, its use was extended for the needs of the CertiCoq certified compiler project, which uses it as its frontend language (CertiCoq compiles Gallina terms to CompCert’s CLight), and the work of Forter and Kunze on extracting Coq terms to a CBV lambda-calculus. However, the syntax currently lacks semantics, be it typing semantics or operational semantics, which should reflect as formal specifications in Coq the semantics of Coq itself. This is an issue for CertiCoq where both a non-deterministic small step semantics and a deterministic call-by-value big step semantics had to be defined and preserved, without an official specification to refer to. Our hope with this work is to remedy this situation and provide a formal semantics of Coq’s implemented type theory, that can independently be refined and studied. By implementing a (partial) independent checker in Coq, we can also help formalize certified translations from Coq to Coq.

Sat 13 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
Tactics and Proof EngineeringCoqPL at Watercourt A
Chair(s): Benjamin Delaware Purdue University
10:30
25m
Talk
A “destruct” Tactic for Mtac2
CoqPL
Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET
File Attached
10:55
25m
Talk
Typed Template Coq
CoqPL
Simon Boulier , Matthieu Sozeau Inria, Nicolas Tabareau Inria, France, Abhishek Anand Cornell 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 Bedford Laval University
File Attached