| 2016 | A Formal Proof of Cauchy's Residue Theorem. Wenda Li, Lawrence C. Paulson |
| 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 | AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic. Bohua Zhan |
| 2016 | Algebraic Numbers in Isabelle/HOL. René Thiemann, Akihisa Yamada |
| 2016 | An Isabelle/HOL Formalisation of Green's Theorem. Mohammad Abdulaziz, Lawrence C. Paulson |
| 2016 | Automatic Functional Correctness Proofs for Functional Search Trees. Tobias Nipkow |
| 2016 | Cardinalities of Finite Relations in Coq. Paul Brunet, Damien Pous, Insa Stucke |
| 2016 | Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. Julian Nagele, Aart Middeldorp |
| 2016 | CoSMed: A Confidentiality-Verified Social Media Platform. Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi |
| 2016 | CoqPIE: An IDE Aimed at Improving Proof Development Productivity - (Rough Diamond). Kenneth Roe, Scott F. Smith |
| 2016 | Equational Reasoning with Applicative Functors. Andreas Lochbihler, Joshua Schneider |
| 2016 | Formalising Semantics for Expected Running Time of Probabilistic Programs. Johannes Hölzl |
| 2016 | Formalization of the Resolution Calculus for First-Order Logic. Anders Schlichtkrull |
| 2016 | Formalized Timed Automata. Simon Wimmer |
| 2016 | Formalizing the Edmonds-Karp Algorithm. Peter Lammich, S. Reza Sefidgar |
| 2016 | Formally Verified Approximations of Definite Integrals. Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote |
| 2016 | From Types to Sets by Local Type Definitions in Higher-Order Logic. Ondrej Kuncar, Andrei Popescu |
| 2016 | HOL Zero's Solutions for Pollack-Inconsistency. Mark Adams |
| 2016 | Hereditarily Finite Sets in Constructive Type Theory. Gert Smolka, Kathrin Stark |
| 2016 | Infeasible Paths Elimination by Symbolic Execution Techniques - Proof of Correctness and Preservation of Paths. Romain Aïssat, Frédéric Voisin, Burkhart Wolff |
| 2016 | Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings Jasmin Christian Blanchette, Stephan Merz |
| 2016 | Mechanical Verification of a Constructive Proof for FLP. Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann |
| 2016 | Modular Dependent Induction in Coq, Mendler-Style. Paolo Torrini |
| 2016 | Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. Thomas Grégoire, Adam Chlipala |
| 2016 | On the Formalization of Fourier Transform in Higher-order Logic. Adnan Rashid, Osman Hasan |
| 2016 | POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). Fahad Ausaf, Roy Dyckhoff, Christian Urban |
| 2016 | Proof Pearl: Bounding Least Common Multiples with Triangles. Hing-Lun Chan, Michael Norrish |
| 2016 | Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah |
| 2016 | The Flow of ODEs. Fabian Immler, Christoph Traut |
| 2016 | Two-Way Automata in Coq. Christian Doczkal, Gert Smolka |
| 2016 | Verified Operational Transformation for Trees. Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov |
| 2016 | Visual Theorem Proving with the Incredible Proof Machine. Joachim Breitner |
| 2016 | What's in a Theorem Name? David Aspinall, Cezary Kaliszyk |