| 2016 | A nominal exploration of intuitionism. | Vincent Rahli, Mark Bickford |
| 2016 | Bisimulation up-to techniques for psi-calculi. | Johannes man Pohjola, Joachim Parrow |
| 2016 | Dependent type practice (invited talk). | Leonardo Mendona de Moura |
| 2016 | A modular, efficient formalisation of real algebraic numbers. | Wenda Li, Lawrence C. Paulson |
| 2016 | Refinement based verification of imperative data structures. | Peter Lammich |
| 2016 | The vampire and the FOOL. | Evgenii Kotelnikov, Laura Kovcs, Giles Reger, Andrei Voronkov |
| 2016 | Towards a mizar environment for isabelle: foundations and language. | Cezary Kaliszyk, Karol Pak, Josef Urban |
| 2016 | A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. | Nathan Fulton, Andr Platzer |
| 2016 | Perspectives on formal verification (invited talk). | Harvey M. Friedman |
| 2016 | Constructing the propositional truncation using non-recursive HITs. | Floris van Doorn |
| 2016 | Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. | Lukasz Czajka |
| 2016 | Formalization of a newton series representation of polynomials. | Cyril Cohen, Boris Djalal |
| 2016 | Higher-order representation predicates in separation logic. | Arthur Charguraud |
| 2016 | Formal verification of control-flow graph flattening. | Sandrine Blazy, Alix Trieu |
| 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 |
| 2015 | Formal Reasoning about the C11 Weak Memory Model. | Viktor Vafeiadis |
| 2015 | Recording Completion for Certificates in Equational Reasoning. | Thomas Sternagel, Sarah Winkler, Harald Zankl |
| 2015 | Clean-Slate Development of Certified OS Kernels. | Zhong Shao |
| 2015 | Completeness and Decidability of de Bruijn Substitution Algebra in Coq. | Steven Schfer, Gert Smolka, Tobias Tebbi |
| 2015 | A Compositional Semantics for Verified Separate Compilation and Linking. | Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jrmie Koenig, Yuchen Fu |
| 2015 | A Framework for Verifying Depth-First Search Algorithms. | Peter Lammich, Ren Neumann |
| 2015 | Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants. | Ondrej Kuncar |
| 2015 | A Typed C11 Semantics for Interactive Theorem Proving. | Robbert Krebbers, Freek Wiedijk |
| 2015 | Certified Connection Tableaux Proofs for HOL Light and TPTP. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | Proving Lock-Freedom Easily and Automatically. | Xiao Jia, Wei Li, Viktor Vafeiadis |