| 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 |
