Program

09:00–09:50

Pierre Corbineau: Generic Automation for the Coq Proof Assistant: Design and Principles   (invited talk)

09:50–10:20

Burak Ekici et al.: Extending SMTCoq, a Certified Checker for SMT

Coffee break

10:50–11:40

Aleksy Schubert: Proof Generation in Propositional Intuitionistic Logic Based upon Automata   (invited talk)

11:40–12:10

Fabian Kunze: Towards the Integration of an Intuitionistic First-Order Prover into Coq

12:10–12:40

Łukasz Czajka and Cezary Kaliszyk: Goal Translation for a Hammer for Coq

Lunch break

14:00–14:40

Revantha Ramanayake: From Axioms to Proof Rules, then Add Quantifiers   (ARQNL invited talk)

14:40–15:10

Jens Otten: Non-Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic   (ARQNL paper)

Short break

15:15–15:45

Ali Assaf et al.: Encoding Proofs in Dedukti: The Case of Coq Proofs

Coffee break

16:15–16:45

Alejandro Aguirre et al.: From F* to SMT

16:45–17:15

Robert Lewis and Leonardo de Moura: Automation and Computation in the Lean Theorem Prover

17:15–17:45

Simon Cruanes and Jasmin Blanchette: Extending Nunchaku to Type Theory

Workshop dinner

Comments are closed