Dr. Hab. Frédéric BLANQUI Research director at Inria Head of 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:

• Encoding type systems with universes in Dedukti
• Translating Rocq or Lean proofs to Isabelle/HOL

News:

• 18 July 2026: Tribute to Gilles Dowek, FLoC'26 workshop, Lisbon, Portugal
• 18-19 July 2026: 21st International Symposium on Logical and Semantic Frameworks with Applications, Lisbon, Portugal
• 22 June - 3 July: Formal Mathematics and Proof Systems Interoperability, Institut Pascal, Orsay, France
• 20 November 2025: new release of hol2dk
• 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
• 16 July 2026: new release of lambdapi
• 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
• 21 January 2025: new release of the HOL-Light Multivariate library in Coq (with the alignment of real numbers)

Duties:

• Chair of the European COST action CA20111 EuroProofNet (>600 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