| 2021 | ITP | Proof Pearl : Playing with the Tower of Hanoi Formally. | Laurent Thry |
| 2019 | ITP | Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. | Ran Chen, Cyril Cohen, Jean-Jacques Lvy, Stephan Merz, Laurent Thry |
| 2019 | ITP | Quantitative Continuity and Computable Analysis in Coq. | Florian Steinberg, Laurent Thry, Holger Thies |
| 2017 | CAV | Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers. | Arthur Blot, Jean-Michel Muller, Laurent Thry |
| 2013 | ITP | A Machine-Checked Proof of the Odd Order Theorem. | Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Franois Garillot, Stphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Thry |
| 2013 | SYNASC | Certified, Efficient and Sharp Univariate Taylor Models in COQ. | rik Martin-Dorel, Laurence Rideau, Laurent Thry, Micaela Mayero, Ioana Pasca |
| 2011 | CPP | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. | Michal Armand, Germain Faure, Benjamin Grgoire, Chantal Keller, Laurent Thry, Benjamin Werner |
| 2010 | ITP | Extending Coq with Imperative Features and Its Application to SAT Verification. | Michal Armand, Benjamin Grgoire, Arnaud Spiwack, Laurent Thry |
| 2006 | CADE | A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. | Benjamin Grgoire, Laurent Thry |
| 2006 | FLOPS | A Computational Approach to Pocklington Certificates in Type Theory. | Benjamin Grgoire, Laurent Thry, Benjamin Werner |
| 1998 | CADE | A Certified Version of Buchberger's Algorithm. | Laurent Thry |
| 1993 | LPAR | Reasoning About the Reals: The Marriage of HOL and Maple. | John Harrison, Laurent Thry |