| 2025 | FlAIRS | Proof Verification with GDV and LambdaPi - It's a Matter of Trust. | Geoff Sutcliffe, Frdric Blanqui, Guillaume Burel |
| 2024 | ITP | Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk). | Frdric Blanqui |
| 2024 | LPAR | Translating HOL-Light proofs to Coq. | Frdric Blanqui |
| 2023 | CSL | Translating Proofs from an Impredicative Type System to a Predicative One. | Thiago Felicissimo, Frdric Blanqui, Ashish Kumar Barnawal |
| 2022 | FSCD | Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. | Frdric Blanqui |
| 2021 | FSCD | Some Axioms for Mathematics. | Frdric Blanqui, Gilles Dowek, milie Grienenberger, Gabriel Hondet, Franois Thir |
| 2020 | FSCD | Type Safety of Rewrite Rules in Dependent Types. | Frdric Blanqui |
| 2020 | FSCD | The New Rewriting Engine of Dedukti (System Description). | Gabriel Hondet, Frdric Blanqui |
| 2011 | CPP | First Steps towards the Certification of an ARM Simulator Using Compcert. | Xiaomu Shi, Jean-Franois Monin, Frdric Tuong, Frdric Blanqui |
| 2009 | CSL | On the Relation between Sized-Types Based Termination and Semantic Labelling. | Frdric Blanqui, Cody Roux |
| 2008 | CSL | The Computability Path Ordering: The End of a Quest. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2007 | CSL | Building Decision Procedures in the Calculus of Inductive Constructions. | Frdric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub |
| 2007 | ESOP | On the Implementation of Construction Functions for Non-free Concrete Data Types. | Frdric Blanqui, Thrse Hardin, Pierre Weis |
| 2007 | LPAR | HORPO with Computability Closure: A Reconstruction. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2006 | FOSSACS | On the Confluence of | Frdric Blanqui, Claude Kirchner, Colin Riba |
| 2006 | LPAR | Higher-Order Termination: From Kruskal to Computability. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2006 | LPAR | Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems. | Frdric Blanqui, Colin Riba |
| 2005 | CSL | Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. | Frdric Blanqui |
| 2001 | LICS | Definitions by Rewriting in the Calculus of Constructions. | Frdric Blanqui |