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 (PhD application form)

News:

• 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
• 13-14 September 2024: EuroProofNet WG4 meeting on proof libraries, Tbilisi, Georgia
• 25 August - 1st September 2024: Invited lecturer at the 14th International School on Rewriting, Obergurgl, Austria
• 29 July 2024: new release of lambdapi
• 29 July 2024: talk on Translating HOL-Light proofs to Coq, Workshop on Libraries of Digital Math, Trimester Program: "Prospects of Formal Mathematics", Hausdorff Institute for Mathematics, Bonn, Germany [video]
• 4 April 2024: Translating HOL-Light proofs to Coq, accepted at LPAR'24
• 5 March 2024: new version of Sharing proofs with predicative theories through universe polymorphic elaboration, with Thiago Felicissimo, 38 pages, accepted for publication in LMCS
• 26 February 2024: new releases of hol2dk and coq-hol-light

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