| 2026 | CPP | Bar Inductive Predicates for Constructive Algebra in Rocq. | Dominique Larchey-Wendling |
| 2023 | ITP | Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. | Dominique Larchey-Wendling, Jean-Franois Monin |
| 2021 | FSCD | Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. | Dominique Larchey-Wendling |
| 2020 | CADE | Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. | Dominik Kirst, Dominique Larchey-Wendling |
| 2019 | CPP | Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. | Yannick Forster, Dominique Larchey-Wendling |
| 2019 | MPC | Certification of Breadth-First Algorithms by Extraction. | Dominique Larchey-Wendling, Ralph Matthes |
| 2018 | CADE | Constructive Decision via Redundancy-Free Proof-Search. | Dominique Larchey-Wendling |
| 2018 | ITP | Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. | Dominique Larchey-Wendling |
| 2017 | ITP | Typing Total Recursive Functions in Coq. | Dominique Larchey-Wendling |
| 2014 | CSR | Separation Logic with One Quantified Variable. | Stphane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Mry |
| 2010 | LICS | The Undecidability of Boolean BI through Phase Semantics. | Dominique Larchey-Wendling, Didier Galmiche |
| 2005 | LPAR | Bounding Resource Consumption with Gdel-Dummett Logics. | Dominique Larchey-Wendling |
| 2004 | CADE | Counter-Model Search in Gdel-Dummett Logics. | Dominique Larchey-Wendling |
| 2002 | CADE | Combining Proof-Search and Counter-Model Construction for Deciding Gdel-Dummett Logic. | Dominique Larchey-Wendling |
| 2001 | CADE | STRIP: Structural Sharing for Efficient Proof-Search. | Dominique Larchey-Wendling, Daniel Mry, Didier Galmiche |