A document-centered approach for an open CASE environment framework connected with the world-wide web. - Frédéric Blanqui (ACM SIGSOFT Softw. Eng. Notes, 1997)

The Calculus of algebraic Constructions. - Frédéric Blanqui; Jean-Pierre Jouannaud; Mitsuhiro Okada (RTA, 1999)

Termination and Confluence of Higher-Order Rewrite Systems. - Frédéric Blanqui (RTA, 2000)

Théorie des types et réécriture. (Type theory and rewriting). - Frédéric Blanqui (2001)

Inductive-data-type systems. - Frédéric Blanqui; Jean-Pierre Jouannaud; Mitsuhiro Okada (Theor. Comput. Sci., 2002)

Rewriting Modulo in Deduction Modulo. - Frédéric Blanqui (RTA, 2003)

A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems. - Frédéric Blanqui (RTA, 2004)

Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. - Frédéric Blanqui (CSL, 2005)

Inductive types in the Calculus of Algebraic Constructions. - Frédéric Blanqui (Fundam. Informaticae, 2005)

Definitions by rewriting in the Calculus of Constructions. - Frédéric Blanqui (Math. Struct. Comput. Sci., 2005)

On the Confluence of lambda-Calculus with Conditional Rewriting. - Frédéric Blanqui; Claude Kirchner; Colin Riba (FoSSaCS, 2006)

Higher-Order Termination: From Kruskal to Computability. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (LPAR, 2006)

Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems. - Frédéric Blanqui; Colin Riba (LPAR, 2006)

(HO)RPO Revisited - Frédéric Blanqui (CoRR, 2006)

Type theory and rewriting - Frédéric Blanqui (CoRR, 2006)

An Isabelle formalization of protocol-independent secrecy with an application to e-commerce - Frédéric Blanqui (CoRR, 2006)

Computability Closure: Ten Years Later. - Frédéric Blanqui (Rewriting, Computation and Proof, 2007)

Building Decision Procedures in the Calculus of Inductive Constructions. - Frédéric Blanqui; Jean-Pierre Jouannaud; Pierre-Yves Strub (CSL, 2007)

On the Implementation of Construction Functions for Non-free Concrete Data Types. - Frédéric Blanqui; Thérèse Hardin; Pierre Weis (ESOP, 2007)

HORPO with Computability Closure: A Reconstruction. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (LPAR, 2007)

The Computability Path Ordering: The End of a Quest. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (CSL, 2008)

From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. - Frédéric Blanqui; Jean-Pierre Jouannaud; Pierre-Yves Strub (IFIP TCS, 2008)

On the Relation between Sized-Types Based Termination and Semantic Labelling. - Frédéric Blanqui; Cody Roux (CSL, 2009)

On the relation between size-based termination and semantic labelling - Frédéric Blanqui; Cody Roux (CoRR, 2009)

Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems. - Keiichirou Kusakari; Yasuo Isogai; Masahiko Sakai; Frédéric Blanqui (IEICE Trans. Inf. Syst., 2009)

On the confluence of lambda-calculus with conditional rewriting. - Frédéric Blanqui; Claude Kirchner; Colin Riba (Theor. Comput. Sci., 2010)

First Steps towards the Certification of an ARM Simulator Using Compcert. - Xiaomu Shi; Jean-François Monin; Frédéric Tuong; Frédéric Blanqui (CPP, 2011)

Designing a CPU model: from a pseudo-formal document to fast code - Frédéric Blanqui; Claude Helmstetter; Vania Joloboff; Jean-François Monin; Xiaomu Shi (CoRR, 2011)

Argument Filterings and Usable Rules in Higher-order Rewrite Systems. - Sho Suzuki; Keiichirou Kusakari; Frédéric Blanqui (Inf. Media Technol., 2011)

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. - Frédéric Blanqui; Adam Koprowski (Math. Struct. Comput. Sci., 2011)

Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité. (Termination of higher-order rewrite systems based on the notion of computability closure). - Frédéric Blanqui (2012)

Automated verification of termination certificates - Frédéric Blanqui; Kim Quyen Ly (CoRR, 2012)

A point on fixpoints in posets. - Frédéric Blanqui (CoRR, 2015)

The computability path ordering. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (Log. Methods Comput. Sci., 2015)

Termination of rewrite relations on λ-terms based on Girard's notion of reducibility. - Frédéric Blanqui (Theor. Comput. Sci., 2016)

Higher-order dependency pairs. - Frédéric Blanqui (CoRR, 2018)

Termination of λΠ modulo rewriting using the size-change principle (work in progress). - Frédéric Blanqui; Guillaume Genestier (CoRR, 2018)

Size-based termination of higher-order rewriting. - Frédéric Blanqui (J. Funct. Program., 2018)

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. - Frédéric Blanqui; Guillaume Genestier; Olivier Hermant (FSCD, 2019)

EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). - Mohamed Yacine El Haddad; Guillaume Burel; Frédéric Blanqui (PxTP, 2019)

Type Safety of Rewrite Rules in Dependent Types. - Frédéric Blanqui (FSCD, 2020)

The New Rewriting Engine of Dedukti (System Description). - Gabriel Hondet; Frédéric Blanqui (FSCD, 2020)

Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. - Gabriel Hondet; Frédéric Blanqui (TYPES, 2020)

The New Rewriting Engine of Dedukti. - Gabriel Hondet; Frédéric Blanqui (CoRR, 2020)

Corrigendum to "Inductive-data-type systems" [Theoret. Comput. Sci. 272 (1-2) (2002) 41-68]. - Frédéric Blanqui; Jean-Pierre Jouannaud; Mitsuhiro Okada (Theor. Comput. Sci., 2020)

Some Axioms for Mathematics. - Frédéric Blanqui; Gilles Dowek; Émilie Grienenberger; Gabriel Hondet; François Thiré (FSCD, 2021)

Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. - Frédéric Blanqui (FSCD, 2022)

Translating Proofs from an Impredicative Type System to a Predicative One. - Thiago Felicissimo; Frédéric Blanqui; Ashish Kumar Barnawal (CSL, 2023)

A modular construction of type theories. - Frédéric Blanqui; Gilles Dowek; Émilie Grienenberger; Gabriel Hondet; François Thiré (Log. Methods Comput. Sci., 2023)

Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk). - Frédéric Blanqui (ITP, 2024)

Translating HOL-Light proofs to Coq. - Frédéric Blanqui (LPAR, 2024)

Sharing proofs with predicative theories through universe-polymorphic elaboration. - Thiago Felicissimo; Frédéric Blanqui (Log. Methods Comput. Sci., 2024)

Proof Verification with GDV and LambdaPi - It's a Matter of Trust. - Geoff Sutcliffe; Frédéric Blanqui; Guillaume Burel (FLAIRS, 2025)