Abstract is missing.
- Proof Assistants and the Dynamic Nature of Formal TheoriesRobert L. Constable. 1-15 [doi]
- + Proof SystemStephan Merz. 16-20 [doi]
- LFSC for SMT Proofs: Work in ProgressAaron Stump, Andrew Reynolds 0001, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang. 21-27 [doi]
- The λΠ-calculus Modulo as a Universal Proof LanguageMathieu Boespflug, Quentin Carbonneaux, Olivier Hermant. 28-43 [doi]
- CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus ModuloMathieu Boespflug, Guillaume Burel. 44-50 [doi]
- System Feature Description: Importing Refutations into the GAPT FrameworkCvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller 0001, Bruno Woltzenlogel Paleo. 51-57 [doi]
- Walking through the Forest: Fast EUF Proof-Checking AlgorithmsFrédéric Besson, Pierre-Emmanuel Cornilleau, Ronan Saillard. 58-64 [doi]