| 2018 | A Coq Formalisation of SQL's Execution Engines. Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins |
| 2018 | A Coq Tactic for Equality Learning in Linear Arithmetic. Sylvain Boulmé, Alexandre Maréchal |
| 2018 | A Formal Equational Theory for Call-By-Push-Value. Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic |
| 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 Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada |
| 2018 | A Formally Verified Solver for Homogeneous Linear Diophantine Equations. Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel |
| 2018 | An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point Theory. Ran Zmigrod, Matthew L. Daggitt, Timothy G. Griffin |
| 2018 | Backwards and Forwards with Separation Logic. Callum Bannister, Peter Höfner, Gerwin Klein |
| 2018 | Boosting the Reuse of Formal Specifications. Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú |
| 2018 | CalcCheck: A Proof Checker for Teaching the "Logical Approach to Discrete Math". Wolfram Kahl |
| 2018 | Efficient Mendler-Style Lambda-Encodings in Cedille. Denis Firsov, Richard Blair, Aaron Stump |
| 2018 | Erratum to: Interactive Theorem Proving. Jeremy Avigad, Assia Mahboubi |
| 2018 | Fast Machine Words in Isabelle/HOL. Andreas Lochbihler |
| 2018 | Formalization of a Polymorphic Subtyping Algorithm. Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers |
| 2018 | Formalizing Implicative Algebras in Coq. Étienne Miquey |
| 2018 | Formalizing Ring Theory in PVS. Andréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino |
| 2018 | HOL Light QE. Jacques Carette, William M. Farmer, Patrick Laskowski |
| 2018 | Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings Jeremy Avigad, Assia Mahboubi |
| 2018 | MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). Simon Wimmer, Johannes Hölzl |
| 2018 | Physical Addressing on Real Hardware in Isabelle/HOL. Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe |
| 2018 | Program Verification in the Presence of Cached Address Translation. Hira Taqdees Syeda, Gerwin Klein |
| 2018 | Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. Dominique Larchey-Wendling |
| 2018 | ProofWatch: Watchlist Guidance for Large Theories in E. Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban |
| 2018 | Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. Jason Gross, Andres Erbsen, Adam Chlipala |
| 2018 | Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. Andreas Lochbihler, Joshua Schneider |
| 2018 | Software Tool Support for Modular Reasoning in Modal Logics of Actions. Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano |
| 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 | Tactics and Certificates in Meta Dedukti. Raphaël Cauderlier |
| 2018 | The Coinductive Formulation of Common Knowledge. Colm Baston, Venanzio Capretta |
| 2018 | Towards Certified Meta-Programming with Typed Template-Coq. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau |
| 2018 | Towards Formal Foundations for Game Theory. Julian Parsert, Cezary Kaliszyk |
| 2018 | Towards Verified Handwritten Calculational Proofs - (Short Paper). Alexandra Mendes, João F. Ferreira |
| 2018 | Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY. Alexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer |
| 2018 | Verification of PCP-Related Computational Reductions in Coq. Yannick Forster, Edith Heiter, Gert Smolka |
| 2018 | Verified Analysis of Random Binary Tree Structures. Manuel Eberl, Max W. Haslbeck, Tobias Nipkow |
| 2018 | Verified Memoization and Dynamic Programming. Simon Wimmer, Shuwei Hu, Tobias Nipkow |
| 2018 | Verified Tail Bounds for Randomized Programs. Joseph Tassarotti, Robert Harper |
| 2018 | Verified Timing Transformations in Synchronous Circuits with \lambda \pi -Ware. João Paulo Pizani Flor, Wouter Swierstra |
| 2018 | Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. Simon Jantsch, Michael Norrish |