| 2018 | A Coq formalization of normalization by evaluation for Martin-Löf type theory. Pawel Wieczorek, Dariusz Biernacki |
| 2018 | A constructive formalisation of Semi-algebraic sets and functions. Boris Djalal |
| 2018 | A formal proof in Coq of a control function for the inverted pendulum. Damien Rouhling |
| 2018 | A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin |
| 2018 | A two-level logic perspective on (simultaneous) substitutions. Kaustuv Chaudhuri |
| 2018 | A verified SAT solver with watched literals using imperative HOL. Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich |
| 2018 | Adapting proof automation to adapt proofs. Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
| 2018 | Binder aware recursion over well-scoped de Bruijn syntax. Jonas Kaiser, Steven Schäfer, Kathrin Stark |
| 2018 | Completeness and decidability of converse PDL in the constructive type theory of Coq. Christian Doczkal, Joachim Bard |
| 2018 | Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada |
| 2018 | Finite sets in homotopy type theory. Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide |
| 2018 | Formal microeconomic foundations and the first welfare theorem. Cezary Kaliszyk, Julian Parsert |
| 2018 | Formal proof of polynomial-time complexity with quasi-interpretations. Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak |
| 2018 | Generic derivation of induction for impredicative encodings in Cedille. Denis Firsov, Aaron Stump |
| 2018 | HOπ in Coq. Sergueï Lenglet, Alan Schmitt |
| 2018 | Large model constructions for second-order ZF in dependent type theory. Dominik Kirst, Gert Smolka |
| 2018 | Mechanising and verifying the WebAssembly specification. Conrad Watt |
| 2018 | Mechanising blockchain consensus. George Pîrlea, Ilya Sergey |
| 2018 | POPLMark reloaded: mechanizing logical relations proofs (invited talk). Brigitte Pientka |
| 2018 | Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018 June Andronick, Amy P. Felty |
| 2018 | Proofs in conflict-driven theory combination. Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar |
| 2018 | Total Haskell is reasonable Coq. Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich |
| 2018 | Towards verifying ethereum smart contract bytecode in Isabelle/HOL. Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples |
| 2018 | Triangulating context lemmas. Craig McLaughlin, James McKinna, Ian Stark |
| 2018 | Œuf: minimizing the Coq extraction TCB. Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman |