Frédéric Blanqui

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