| 2019 | A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. Véronique Benzaken, Evelyne Contejean |
| 2019 | A formal proof of hensel's lemma over the p-adic integers. Robert Y. Lewis |
| 2019 | A linear logical framework in hybrid (invited talk). Amy P. Felty |
| 2019 | A proof-theoretic approach to certifying skolemization. Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller |
| 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 | A verified protocol buffer compiler. Qianchuan Ye, Benjamin Delaware |
| 2019 | A verified prover based on ordered resolution. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel |
| 2019 | Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. Kathrin Stark, Steven Schäfer, Jonas Kaiser |
| 2019 | Call-by-push-value in coq: operational, equational, and denotational theory. Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark |
| 2019 | Certified ACKBO. Alexander Lochmann, Christian Sternagel |
| 2019 | Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. Yannick Forster, Dominique Larchey-Wendling |
| 2019 | Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. Wenda Li, Lawrence C. Paulson |
| 2019 | Dynamic class initialization semantics: a jinja extension. Susannah Mansky, Elsa L. Gunter |
| 2019 | Eliminating reflection from type theory. Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau |
| 2019 | Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. Sandrine Blazy, Rémi Hutin |
| 2019 | Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). Jasmin Christian Blanchette |
| 2019 | Formally verified big step semantics out of x86-64 binaries. Ian Roessle, Freek Verbeek, Binoy Ravindran |
| 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 | On synthetic undecidability in coq, with an application to the entscheidungsproblem. Yannick Forster, Dominik Kirst, Gert Smolka |
| 2019 | Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019 Assia Mahboubi, Magnus O. Myreen |
| 2019 | Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. Fabian Immler, Bohua Zhan |
| 2019 | Verified solving and asymptotics of linear recurrences. Manuel Eberl |