| 2017 | How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. | David Butler, David Aspinall, Adri Gascn |
| 2017 | Formal Verification of a Floating-Point Expansion Renormalization Algorithm. | Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu |
| 2017 | CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2017 | Formalization of the Lindemann-Weierstrass Theorem. | Sophie Bernard |
| 2017 | Certifying Standard and Stratified Datalog Inference Engines in SSReflect. | Vronique Benzaken, Evelyne Contejean, Stefania Dumbrava |
| 2017 | A Formal Proof of the Expressiveness of Deep Learning. | Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow |
| 2017 | A Formalization of Convex Polyhedra Based on the Simplex Method. | Xavier Allamigeon, Ricardo D. Katz |
| 2016 | AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic. | Bohua Zhan |
| 2016 | Formalized Timed Automata. | Simon Wimmer |
| 2016 | Modular Dependent Induction in Coq, Mendler-Style. | Paolo Torrini |
| 2016 | Algebraic Numbers in Isabelle/HOL. | Ren Thiemann, Akihisa Yamada |
| 2016 | Hereditarily Finite Sets in Constructive Type Theory. | Gert Smolka, Kathrin Stark |
| 2016 | Verified Operational Transformation for Trees. | Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov |
| 2016 | Formalization of the Resolution Calculus for First-Order Logic. | Anders Schlichtkrull |
| 2016 | CoqPIE: An IDE Aimed at Improving Proof Development Productivity - (Rough Diamond). | Kenneth Roe, Scott F. Smith |
| 2016 | A Framework for the Automatic Formal Verification of Refinement from Cogent to C. | Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein |
| 2016 | On the Formalization of Fourier Transform in Higher-order Logic. | Adnan Rashid, Osman Hasan |
| 2016 | Automatic Functional Correctness Proofs for Functional Search Trees. | Tobias Nipkow |
| 2016 | Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. | Julian Nagele, Aart Middeldorp |
| 2016 | Formally Verified Approximations of Definite Integrals. | Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote |
| 2016 | Equational Reasoning with Applicative Functors. | Andreas Lochbihler, Joshua Schneider |
| 2016 | A Formal Proof of Cauchy's Residue Theorem. | Wenda Li, Lawrence C. Paulson |
| 2016 | Formalizing the Edmonds-Karp Algorithm. | Peter Lammich, S. Reza Sefidgar |
| 2016 | From Types to Sets by Local Type Definitions in Higher-Order Logic. | Ondrej Kuncar, Andrei Popescu |
| 2016 | The Flow of ODEs. | Fabian Immler, Christoph Traut |