- Alejandro Aguirre, Cătălin Hriţcu, Chantal Keller, and Nikhil Swamy
From F* to SMT - Simon Cruanes and Jasmin Christian Blanchette
Extending Nunchaku to Type Theory - Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, and Jiaxiang Liu
Encoding Proofs in Dedukti: the Case of Coq Proofs - Fabian Kunze
Towards the Integration of an Intuitionistic First-Order Prover into Coq - Łukasz Czajka and Cezary Kaliszyk
Goal Translation for a Hammer for Coq - Burak Ekici, Alain Mebsout, Cesare Tinelli, and Chantal Keller
Extending SMTCoq, a Certified Checker for SMT - Robert Lewis and Leonardo de Moura
Automation and Computation in the Lean Theorem Prover
The EPTCS proceedings comprise a selection of the papers.