| 2018 | A Coq formalization of normalization by evaluation for Martin-Lf type theory. | Pawel Wieczorek, Dariusz Biernacki |
| 2018 | Mechanising and verifying the WebAssembly specification. | Conrad Watt |
| 2018 | Total Haskell is reasonable Coq. | Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich |
| 2018 | A formal proof in Coq of a control function for the inverted pendulum. | Damien Rouhling |
| 2018 | Adapting proof automation to adapt proofs. | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
| 2018 | Mechanising blockchain consensus. | George Prlea, Ilya Sergey |
| 2018 | POPLMark reloaded: mechanizing logical relations proofs (invited talk). | Brigitte Pientka |
| 2018 | Œuf: minimizing the Coq extraction TCB. | Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman |
| 2018 | Triangulating context lemmas. | Craig McLaughlin, James McKinna, Ian Stark |
| 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 | Formal microeconomic foundations and the first welfare theorem. | Cezary Kaliszyk, Julian Parsert |
| 2018 | Binder aware recursion over well-scoped de Bruijn syntax. | Jonas Kaiser, Steven Schfer, Kathrin Stark |
| 2018 | A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. | Niklas Grimm, Kenji Maillard, Cdric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Bguelin |
| 2018 | Finite sets in homotopy type theory. | Dan Frumin, Herman Geuvers, Lon Gondelman, Niels van der Weide |
| 2018 | A verified SAT solver with watched literals using imperative HOL. | Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich |
| 2018 | Generic derivation of induction for impredicative encodings in Cedille. | Denis Firsov, Aaron Stump |
| 2018 | Formal proof of polynomial-time complexity with quasi-interpretations. | Hugo Fre, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak |
| 2018 | Completeness and decidability of converse PDL in the constructive type theory of Coq. | Christian Doczkal, Joachim Bard |
| 2018 | A constructive formalisation of Semi-algebraic sets and functions. | Boris Djalal |
| 2018 | Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). | Jose Divasn, Sebastiaan J. C. Joosten, Ondrej Kuncar, Ren Thiemann, Akihisa Yamada |
| 2018 | A two-level logic perspective on (simultaneous) substitutions. | Kaustuv Chaudhuri |
| 2018 | Proofs in conflict-driven theory combination. | Maria Paola Bonacina, Stphane Graham-Lengrand, Natarajan Shankar |
| 2018 | Towards verifying ethereum smart contract bytecode in Isabelle/HOL. | Sidney Amani, Myriam Bgel, Maksym Bortin, Mark Staples |
| 2017 | Formalization of Karp-Miller tree construction on petri nets. | Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto |