| 2016 | A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. Nathan Fulton, André Platzer |
| 2016 | A modular, efficient formalisation of real algebraic numbers. Wenda Li, Lawrence C. Paulson |
| 2016 | A nominal exploration of intuitionism. Vincent Rahli, Mark Bickford |
| 2016 | A unified Coq framework for verifying C programs with floating-point computations. Tahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard Lethin |
| 2016 | A verified algorithm for detecting conflicts in XACML access control rules. Michel St-Martin, Amy P. Felty |
| 2016 | Axiomatic semantics for compiler verification. Steven Schäfer, Sigurd Schneider, Gert Smolka |
| 2016 | Bisimulation up-to techniques for psi-calculi. Johannes Åman Pohjola, Joachim Parrow |
| 2016 | Constructing the propositional truncation using non-recursive HITs. Floris van Doorn |
| 2016 | Dependent type practice (invited talk). Leonardo Mendonça de Moura |
| 2016 | Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub |
| 2016 | Formal verification of control-flow graph flattening. Sandrine Blazy, Alix Trieu |
| 2016 | Formalization of a newton series representation of polynomials. Cyril Cohen, Boris Djalal |
| 2016 | Formalizing jordan normal forms in Isabelle/HOL. René Thiemann, Akihisa Yamada |
| 2016 | Higher-order representation predicates in separation logic. Arthur Charguéraud |
| 2016 | Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. Lukasz Czajka |
| 2016 | Perspectives on formal verification (invited talk). Harvey M. Friedman |
| 2016 | Planning for change in a formal verification of the raft consensus protocol. Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson |
| 2016 | Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016 Jeremy Avigad, Adam Chlipala |
| 2016 | Refinement based verification of imperative data structures. Peter Lammich |
| 2016 | The vampire and the FOOL. Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov |
| 2016 | Towards a mizar environment for isabelle: foundations and language. Cezary Kaliszyk, Karol Pak, Josef Urban |