| 2017 | A Formal Proof in Coq of LaSalle's Invariance Principle. Cyril Cohen, Damien Rouhling |
| 2017 | A Formal Proof of the Expressiveness of Deep Learning. Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow |
| 2017 | A Formalisation of Consistent Consequence for Boolean Equation Systems. Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse |
| 2017 | A Formalization of Convex Polyhedra Based on the Simplex Method. Xavier Allamigeon, Ricardo D. Katz |
| 2017 | A Formalized General Theory of Syntax with Bindings. Lorenzo Gheri, Andrei Popescu |
| 2017 | A Verified Generational Garbage Collector for CakeML. Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola |
| 2017 | Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System. Moa Johansson |
| 2017 | Automating Formalization by Statistical and Semantic Parsing of Mathematics. Cezary Kaliszyk, Josef Urban, Jirí Vyskocil |
| 2017 | Bellerophon: Tactical Theorem Proving for Hybrid Systems. Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer |
| 2017 | Categoricity Results for Second-Order ZF in Dependent Type Theory. Dominik Kirst, Gert Smolka |
| 2017 | Certifying Standard and Stratified Datalog Inference Engines in SSReflect. Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava |
| 2017 | CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. Frédéric Besson, Sandrine Blazy, Pierre Wilke |
| 2017 | Effect Polymorphism in Higher-Order Logic (Proof Pearl). Andreas Lochbihler |
| 2017 | Efficient, Verified Checking of Propositional Proofs. Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler |
| 2017 | FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. Raphaël Cauderlier, Catherine Dubois |
| 2017 | Formal Verification of a Floating-Point Expansion Renormalization Algorithm. Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu |
| 2017 | Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. Bohua Zhan |
| 2017 | Formalization of the Lindemann-Weierstrass Theorem. Sophie Bernard |
| 2017 | Formalizing Basic Quaternionic Analysis. Andrea Gabrielli, Marco Maggesi |
| 2017 | Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics. Yanni Kouskoulas, Daniel Genin, Aurora C. Schmidt, Jean-Baptiste Jeannin |
| 2017 | Homotopy Type Theory in Lean. Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz |
| 2017 | How to Get More Out of Your Oracles. Luís Cruz-Filipe, Kim S. Larsen, Peter Schneider-Kamp |
| 2017 | How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. David Butler, David Aspinall, Adrià Gascón |
| 2017 | Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings Mauricio Ayala-Rincón, César A. Muñoz |
| 2017 | Making PVS Accessible to Generic Services by Interpretation in a Universal Format. Michael Kohlhase, Dennis Müller, Sam Owre, Florian Rabe |
| 2017 | Proof Certificates in PVS. Frédéric Gilbert |
| 2017 | Proof Tactics for Assertions in Separation Logic. Zhe Hou, David Sanán, Alwen Tiu, Yang Liu |
| 2017 | Schulze Voting as Evidence Carrying Computation. Dirk Pattinson, Mukesh Tiwari |
| 2017 | Typing Total Recursive Functions in Coq. Dominique Larchey-Wendling |
| 2017 | Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. Laureano Lambán, Francisco J. Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina |
| 2017 | Verified Spilling and Translation Validation with Repair. Julian Rosemann, Sigurd Schneider, Sebastian Hack |
| 2017 | Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek |
| 2017 | Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. Yannick Forster, Gert Smolka |