Frédéric Blanqui

According to our database, Frédéric Blanqui authored at least 52 papers between 1997 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Sharing proofs with predicative theories through universe-polymorphic elaboration.

Thiago Felicissimo, Frédéric Blanqui

Log. Methods Comput. Sci., 2024

Translating HOL-Light proofs to Coq.

Frédéric Blanqui

Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk).

Frédéric Blanqui

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

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 Proofs from an Impredicative Type System to a Predicative One.

Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal

Proceedings of the 31st EACSL Annual Conference on Computer Science Logic, 2023

2022

Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity.

Frédéric Blanqui

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021

Some Axioms for Mathematics.

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, François Thiré

Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

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

The New Rewriting Engine of Dedukti.

Gabriel Hondet, Frédéric Blanqui

CoRR, 2020

Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory.

Gabriel Hondet, Frédéric Blanqui

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

The New Rewriting Engine of Dedukti (System Description).

Gabriel Hondet, Frédéric Blanqui

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Type Safety of Rewrite Rules in Dependent Types.

Frédéric Blanqui

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

2019

EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract).

Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui

Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting.

Frédéric Blanqui, Guillaume Genestier, Olivier Hermant

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018

Size-based termination of higher-order rewriting.

Frédéric Blanqui

J. Funct. Program., 2018

Termination of λΠ modulo rewriting using the size-change principle (work in progress).

Frédéric Blanqui, Guillaume Genestier

CoRR, 2018

Higher-order dependency pairs.

Frédéric Blanqui

CoRR, 2018

2016

Termination of rewrite relations on λ-terms based on Girard's notion of reducibility.

Frédéric Blanqui

Theor. Comput. Sci., 2016

2015

The computability path ordering.

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Log. Methods Comput. Sci., 2015

A point on fixpoints in posets.

Frédéric Blanqui

CoRR, 2015

2012

Automated verification of termination certificates

Frédéric Blanqui, Kim Quyen Ly

CoRR, 2012

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

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

Argument Filterings and Usable Rules in Higher-order Rewrite Systems.

Sho Suzuki, Keiichirou Kusakari, Frédéric Blanqui

Inf. Media Technol., 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

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

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

On the confluence of lambda-calculus with conditional rewriting.

Frédéric Blanqui, Claude Kirchner, Colin Riba

Theor. Comput. Sci., 2010

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 relation between size-based termination and semantic labelling

Frédéric Blanqui, Cody Roux

CoRR, 2009

On the Relation between Sized-Types Based Termination and Semantic Labelling.

Frédéric Blanqui, Cody Roux

Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

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

Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

The Computability Path Ordering: The End of a Quest.

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

2007

HORPO with Computability Closure: A Reconstruction.

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the Logic for Programming, 2007

On the Implementation of Construction Functions for Non-free Concrete Data Types.

Frédéric Blanqui, Thérèse Hardin, Pierre Weis

Proceedings of the Programming Languages and Systems, 2007

Building Decision Procedures in the Calculus of Inductive Constructions.

Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

Computability Closure: Ten Years Later.

Frédéric Blanqui

Proceedings of the Rewriting, 2007

2006

An Isabelle formalization of protocol-independent secrecy with an application to e-commerce

Frédéric Blanqui

CoRR, 2006

Type theory and rewriting

Frédéric Blanqui

CoRR, 2006

(HO)RPO Revisited

Frédéric Blanqui

CoRR, 2006

Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems.

Frédéric Blanqui, Colin Riba

Proceedings of the Logic for Programming, 2006

Higher-Order Termination: From Kruskal to Computability.

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the Logic for Programming, 2006

On the Confluence of <i>lambda</i>-Calculus with Conditional Rewriting.

Frédéric Blanqui, Claude Kirchner, Colin Riba

Proceedings of the Foundations of Software Science and Computation Structures, 2006

2005

Definitions by rewriting in the Calculus of Constructions.

Frédéric Blanqui

Math. Struct. Comput. Sci., 2005

Inductive types in the Calculus of Algebraic Constructions.

Frédéric Blanqui

Fundam. Informaticae, 2005

Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations.

Frédéric Blanqui

Proceedings of the Computer Science Logic, 19th International Workshop, 2005

2004

A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems.

Frédéric Blanqui

Proceedings of the Rewriting Techniques and Applications, 15th International Conference, 2004

2003

Rewriting Modulo in Deduction Modulo.

Frédéric Blanqui

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002

Inductive-data-type systems.

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada

Theor. Comput. Sci., 2002

2001

Théorie des types et réécriture. (Type theory and rewriting).

Frédéric Blanqui

PhD thesis, 2001

2000

Termination and Confluence of Higher-Order Rewrite Systems.

Frédéric Blanqui

Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

1999

The Calculus of algebraic Constructions.

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada

Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

1997

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