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:

• 15-16 September 2025: EuroProofNet Workshop on Proof Libraries
• 8-11 September 2025: 1st International School on Logical Frameworks and Proof Systems Interoperability (LFPSI'25)
• 8-19 September 2025: Final EuroProofNet Symposium
• 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
• 4 February 2025: new release of lambdapi and lambdapi-stdlib
• 21 January 2025: new release of the ">translation of the HOL-Light Multivariate library in Coq (with alignment of real numbers)

Duties:

• Chair of the European COST action CA20111 EuroProofNet (>578 participants from 47 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