Frédéric Blanqui

ORCID

Publication Activity (10 Years)

Years Active: 1997-2023
Publications (10 Years): 25

Top Venues

CoRR

FSCD

Log. Methods Comput. Sci.

Theor. Comput. Sci.

University of Paris-Sud, Orsay, France (PHD)

Education History

University of Paris-Sud, Orsay, France

PHD

Publications

Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal
Translating Proofs from an Impredicative Type System to a Predicative One. CSL (2023)
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
A modular construction of type theories. Log. Methods Comput. Sci. 19 (1) (2023)
Thiago Felicissimo, Frédéric Blanqui
Sharing proofs with predicative theories through universe polymorphic elaboration. CoRR (2023)
Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal
Translating proofs from an impredicative type system to a predicative one. CoRR (2022)
Frédéric Blanqui
Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. FSCD (2022)
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
Some Axioms for Mathematics. FSCD (2021)
Gabriel Hondet, Frédéric Blanqui
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. CoRR (2021)
Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré
Some axioms for mathematics. CoRR (2021)
Gabriel Hondet, Frédéric Blanqui
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. TYPES (2020)
Gabriel Hondet, Frédéric Blanqui
The New Rewriting Engine of Dedukti. CoRR (2020)
Frédéric Blanqui
Type safety of rewrite rules in dependent types. CoRR (2020)
Frédéric Blanqui
Type Safety of Rewrite Rules in Dependent Types. FSCD (2020)
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
Corrigendum to "Inductive-data-type systems" [Theoret. Comput. Sci. 272 (1-2) (2002) 41-68]. Theor. Comput. Sci. 817 (2020)
Gabriel Hondet, Frédéric Blanqui
The New Rewriting Engine of Dedukti (System Description). FSCD (2020)
Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. FSCD (2019)
Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. CoRR (2019)
Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). PxTP (2019)
Frédéric Blanqui
Higher-order dependency pairs. CoRR (2018)
Frédéric Blanqui
Size-based termination of higher-order rewriting. CoRR (2018)
Frédéric Blanqui, Guillaume Genestier
Termination of λΠ modulo rewriting using the size-change principle (work in progress). CoRR (2018)
Frédéric Blanqui
Size-based termination of higher-order rewriting. J. Funct. Program. 28 (2018)
Frédéric Blanqui
Termination of rewrite relations on λ-terms based on Girard's notion of reducibility. Theor. Comput. Sci. 611 (2016)
Frédéric Blanqui
A point on fixpoints in posets. CoRR (2015)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
The computability path ordering. Log. Methods Comput. Sci. 11 (4) (2015)
Frédéric Blanqui
Termination of rewrite relations on $λ$-terms based on Girard's notion of reducibility. CoRR (2015)
Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui
First steps towards the certification of an ARM simulator using Compcert CoRR (2012)
Frédéric Blanqui, Adam Koprowski
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. CoRR (2012)
Frédéric Blanqui, Kim Quyen Ly
Automated verification of termination certificates CoRR (2012)
Frédéric Blanqui, Adam Koprowski
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21 (4) (2011)
Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, Frédéric Blanqui
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems CoRR (2011)
Sho Suzuki, Keiichirou Kusakari, Frédéric Blanqui
Argument filterings and usable rules in higher-order rewrite systems CoRR (2011)
Frédéric Blanqui, Claude Kirchner, Colin Riba
On the confluence of lambda-calculus with conditional rewriting CoRR (2011)
Frédéric Blanqui, Claude Helmstetter, Vania Joloboff, Jean-François Monin, Xiaomu Shi
Designing a CPU model: from a pseudo-formal document to fast code CoRR (2011)
Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui
First Steps towards the Certification of an ARM Simulator Using Compcert. CPP (2011)
Frédéric Blanqui, Claude Kirchner, Colin Riba
On the confluence of lambda-calculus with conditional rewriting. Theor. Comput. Sci. 411 (37) (2010)
Frédéric Blanqui, Cody Roux
On the relation between size-based termination and semantic labelling CoRR (2009)
Frédéric Blanqui, Cody Roux
On the Relation between Sized-Types Based Termination and Semantic Labelling. CSL (2009)
Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, Frédéric Blanqui
Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems. IEICE Trans. Inf. Syst. (10) (2009)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
The computability path ordering: the end of a quest CoRR (2008)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
The Computability Path Ordering: The End of a Quest. CSL (2008)
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures CoRR (2008)
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. IFIP TCS (2008)
Frédéric Blanqui
Computability Closure: Ten Years Later CoRR (2007)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
HORPO with Computability Closure: A Reconstruction. LPAR (2007)
Frédéric Blanqui
Computability Closure: Ten Years Later. Rewriting, Computation and Proof (2007)
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
Building Decision Procedures in the Calculus of Inductive Constructions CoRR (2007)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
HORPO with Computability Closure : A Reconstruction CoRR (2007)
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
Building Decision Procedures in the Calculus of Inductive Constructions. CSL (2007)
Frédéric Blanqui, Thérèse Hardin, Pierre Weis
On the Implementation of Construction Functions for Non-free Concrete Data Types. ESOP (2007)
Frédéric Blanqui, Thérèse Hardin, Pierre Weis
On the implementation of construction functions for non-free concrete data types CoRR (2007)
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
Inductive-data-type Systems CoRR (2006)
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
The Calculus of Algebraic Constructions CoRR (2006)
Frédéric Blanqui, Claude Kirchner, Colin Riba
-Calculus with Conditional Rewriting. FoSSaCS (2006)
Frédéric Blanqui, Colin Riba
Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems. LPAR (2006)
Frédéric Blanqui
Rewriting modulo in Deduction modulo CoRR (2006)
Frédéric Blanqui
Definitions by rewriting in the Calculus of Constructions CoRR (2006)
Frédéric Blanqui
Termination and Confluence of Higher-Order Rewrite Systems CoRR (2006)
Frédéric Blanqui
Inductive types in the Calculus of Algebraic Constructions CoRR (2006)
Frédéric Blanqui
Definitions by Rewriting in the Calculus of Constructions CoRR (2006)
Frédéric Blanqui
A type-based termination criterion for dependently-typed higher-order rewrite systems CoRR (2006)
Frédéric Blanqui, Claude Kirchner, Colin Riba
On the confluence of lambda-calculus with conditional rewriting CoRR (2006)
Frédéric Blanqui
An Isabelle formalization of protocol-independent secrecy with an application to e-commerce CoRR (2006)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
Higher-Order Termination: From Kruskal to Computability. LPAR (2006)
Frédéric Blanqui
Inductive types in the Calculus of Algebraic Constructions CoRR (2006)
Frédéric Blanqui, Colin Riba
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems CoRR (2006)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
Higher-Order Termination: from Kruskal to Computability CoRR (2006)
Frédéric Blanqui
(HO)RPO Revisited CoRR (2006)
Frédéric Blanqui
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations CoRR (2006)
Frédéric Blanqui
Type theory and rewriting CoRR (2006)
Frédéric Blanqui
Inductive types in the Calculus of Algebraic Constructions. Fundam. Informaticae 65 (1-2) (2005)
Frédéric Blanqui
Definitions by rewriting in the Calculus of Constructions. Math. Struct. Comput. Sci. 15 (1) (2005)
Frédéric Blanqui
Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. CSL (2005)
Frédéric Blanqui
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems. RTA (2004)
Frédéric Blanqui
Rewriting Modulo in Deduction Modulo. RTA (2003)
Frédéric Blanqui
Inductive Types in the Calculus of Algebraic Constructions. TLCA (2003)
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
Inductive-data-type systems. Theor. Comput. Sci. 272 (1-2) (2002)
Frédéric Blanqui
Definitions by Rewriting in the Calculus of Constructions. LICS (2001)
Frédéric Blanqui
Termination and Confluence of Higher-Order Rewrite Systems. RTA (2000)
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
The Calculus of algebraic Constructions. RTA (1999)
Frédéric Blanqui
A document-centered approach for an open CASE environment framework connected with the world-wide web. ACM SIGSOFT Softw. Eng. Notes 22 (2) (1997)

Frédéric Blanqui.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Frédéric Blanqui