| 2018 | Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. | Andreas Lochbihler, Joshua Schneider |
| 2018 | Fast Machine Words in Isabelle/HOL. | Andreas Lochbihler |
| 2018 | Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. | Dominique Larchey-Wendling |
| 2018 | Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). | Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen |
| 2018 | Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY. | Alexander Knppel, Thomas Thm, Carsten Immanuel Pardylla, Ina Schaefer |
| 2018 | CalcCheck: A Proof Checker for Teaching the "Logical Approach to Discrete Math". | Wolfram Kahl |
| 2018 | Verifying the LTL to Bchi Automata Translation via Very Weak Alternating Automata. | Simon Jantsch, Michael Norrish |
| 2018 | Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. | Jason Gross, Andres Erbsen, Adam Chlipala |
| 2018 | ProofWatch: Watchlist Guidance for Large Theories in E. | Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban |
| 2018 | Verified Timing Transformations in Synchronous Circuits with \lambda \pi -Ware. | Joo Paulo Pizani Flor, Wouter Swierstra |
| 2018 | Efficient Mendler-Style Lambda-Encodings in Cedille. | Denis Firsov, Richard Blair, Aaron Stump |
| 2018 | Verified Analysis of Random Binary Tree Structures. | Manuel Eberl, Max W. Haslbeck, Tobias Nipkow |
| 2018 | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. | Christian Doczkal, Guillaume Combette, Damien Pous |
| 2018 | A Formalization of the LLL Basis Reduction Algorithm. | Jose Divasn, Sebastiaan J. C. Joosten, Ren Thiemann, Akihisa Yamada |
| 2018 | Tactics and Certificates in Meta Dedukti. | Raphal Cauderlier |
| 2018 | HOL Light QE. | Jacques Carette, William M. Farmer, Patrick Laskowski |
| 2018 | A Coq Tactic for Equality Learning in Linear Arithmetic. | Sylvain Boulm, Alexandre Marchal |
| 2018 | A Coq Formalisation of SQL's Execution Engines. | Vronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins |
| 2018 | The Coinductive Formulation of Common Knowledge. | Colm Baston, Venanzio Capretta |
| 2018 | Backwards and Forwards with Separation Logic. | Callum Bannister, Peter Hfner, Gerwin Klein |
| 2018 | Software Tool Support for Modular Reasoning in Modal Logics of Actions. | Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano |
| 2018 | Erratum to: Interactive Theorem Proving. | Jeremy Avigad, Assia Mahboubi |
| 2018 | Towards Certified Meta-Programming with Typed Template-Coq. | Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau |
| 2018 | Physical Addressing on Real Hardware in Isabelle/HOL. | Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe |
| 2018 | Verification of PCP-Related Computational Reductions in Coq. | Yannick Forster, Edith Heiter, Gert Smolka |