| 2017 | A Coq formal proof of the LaxMilgram theorem. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero |
| 2017 | A formalization of the Berlekamp-Zassenhaus factorization algorithm. Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada |
| 2017 | A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. Érik Martin-Dorel, Pierre Roux |
| 2017 | Automatic cyclic termination proofs for recursive procedures in separation logic. Reuben N. S. Rowe, James Brotherston |
| 2017 | BliStrTune: hierarchical invention of theorem proving strategies. Jan Jakubuv, Josef Urban |
| 2017 | Complx: a verification framework for concurrent imperative programs. Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong |
| 2017 | Equivalence of system f and ź2 in Coq based on context morphism lemmas. Jonas Kaiser, Tobias Tebbi, Gert Smolka |
| 2017 | Formal foundations of 3D geometry to model robot manipulators. Reynald Affeldt, Cyril Cohen |
| 2017 | Formalising real numbers in homotopy type theory. Gaëtan Gilbert |
| 2017 | Formalization of Karp-Miller tree construction on petri nets. Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto |
| 2017 | Formally verified differential dynamic logic. Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer |
| 2017 | Lifting proof-relevant unification to higher dimensions. Jesper Cockx, Dominique Devriese |
| 2017 | Markov processes in Isabelle/HOL. Johannes Hölzl |
| 2017 | Mechanized verification of preemptive OS kernels (invited talk). Xinyu Feng |
| 2017 | Porting the HOL light analysis library: some lessons (invited talk). Lawrence C. Paulson |
| 2017 | Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017 Yves Bertot, Viktor Vafeiadis |
| 2017 | The HoTT library: a formalization of homotopy type theory in Coq. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters |
| 2017 | The next 700 syntactical models of type theory. Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau |
| 2017 | Type-and-scope safe programs and their proofs. Guillaume Allais, James Chapman, Conor McBride, James McKinna |
| 2017 | Verified compilation of CakeML to multiple machine-code targets. Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar |
| 2017 | Verifying a hash table and its iterators in higher-order separation logic. François Pottier |
| 2017 | Verifying dynamic race detection. William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti |