| 2020 | Frying the egg, roasting the chicken: unit deletions in DRAT proofs. | Johannes Altmanninger, Adrian Rebola-Pardo |
| 2020 | Coq la carte: a practical approach to modular syntax with binders. | Yannick Forster, Kathrin Stark |
| 2020 | Verified programming of Turing machines in Coq. | Yannick Forster, Fabian Kunze, Maxi Wuttke |
| 2020 | Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. | David Butler, David Aspinall, Adri Gascn |
| 2019 | A verified protocol buffer compiler. | Qianchuan Ye, Benjamin Delaware |
| 2019 | Eliminating reflection from type theory. | Tho Winterhalter, Matthieu Sozeau, Nicolas Tabareau |
| 2019 | Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. | Kathrin Stark, Steven Schfer, Jonas Kaiser |
| 2019 | A verified prover based on ordered resolution. | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel |
| 2019 | Formally verified big step semantics out of x86-64 binaries. | Ian Roessle, Freek Verbeek, Binoy Ravindran |
| 2019 | Dynamic class initialization semantics: a jinja extension. | Susannah Mansky, Elsa L. Gunter |
| 2019 | Certified ACKBO. | Alexander Lochmann, Christian Sternagel |
| 2019 | Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. | Wenda Li, Lawrence C. Paulson |
| 2019 | A formal proof of hensel's lemma over the p-adic integers. | Robert Y. Lewis |
| 2019 | From C to interaction trees: specifying, verifying, and testing a networked server. | Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honor, William Mansky, Benjamin C. Pierce, Steve Zdancewic |
| 2019 | Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. | Fabian Immler, Bohua Zhan |
| 2019 | Call-by-push-value in coq: operational, equational, and denotational theory. | Yannick Forster, Steven Schfer, Simon Spies, Kathrin Stark |
| 2019 | Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. | Yannick Forster, Dominique Larchey-Wendling |
| 2019 | A linear logical framework in hybrid (invited talk). | Amy P. Felty |
| 2019 | A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL. | Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp |
| 2019 | Verified solving and asymptotics of linear recurrences. | Manuel Eberl |
| 2019 | A proof-theoretic approach to certifying skolemization. | Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller |
| 2019 | Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. | Sandrine Blazy, Rmi Hutin |
| 2019 | Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). | Jasmin Christian Blanchette |
| 2019 | A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. | Vronique Benzaken, Evelyne Contejean |
| 2019 | On synthetic undecidability in coq, with an application to the entscheidungsproblem. | Yannick Forster, Dominik Kirst, Gert Smolka |