Dr. Hab. Frédéric BLANQUI Research director at Inria Project Deducteam Chair of EuroProofNet

Research interests: proof system interoperability, proof assistants, rewriting, type theory, λ-calculus, termination, ...

Publications  | Talks  | Software  | Teaching  | Students  | Useful links  | Homepages  | PC

Internship/PhD/postdoc proposals:

• Proving the equivalence of type and function definitions automatically in Coq or Lean (PhD application form)
• Translating Isabelle proofs with type classes and locales to Coq or Lean (PhD application form)
• Translating Coq or Lean proofs to Isabelle/HOL (PhD application form)

News:

• 11 March 2025: Proof Verification with GDV and LambdaPi, It's a Matter of Trust, with Geoff Sutcliffe and Guillaume Burel, accepted to FLAIRS'25
• 3 March 2025: Towards the Verification of Higher-Order Logic Automated Reasoning, with Melanie Taprogge, Alexander Steen
• 4 February 2025: new release of lambdapi and lambdapi-stdlib
• 17 December 2024: complete translation of HOL-Light base library in Coq
• 13 September 2024: Translating libraries of definitions and theorems between proof systems (invited talk), 15th International Conference on Interactive Theorem Proving, (ITP'24) , Tbilisi, Georgia

Duties:

• Chair of the European COST action CA20111 EuroProofNet (>500 participants from 44 countries)
• French PI of the 2024-2026 INRIA-AIST associated team ICI
• Assistant director of the Paris-Saclay doctoral school of computer science in charge of the budget
• Member of the scientific committee of Inria Paris-Saclay
• Member of the steering committee of ISR
• Member of the IFIP WG1.6 on rewriting

LMF, 4 avenue des Sciences, 91190 Gif-sur-Yvette, France Office 3U61, Tel: +33 (0) 1 81 87 54 35 Email: frederic . blanqui (a) inria . fr How to come? Transport - Campus