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:

• Certifying PVS proofs
• Inter-system translation of recursive functions
• Interoperability of proof systems based on higher-order logic [apply]

News:

• 18-20 September 2024: 19th Logical and Semantic Frameworks with Applications, Goiânia, Brazil
• 25 August - 1st September 2024: Invited lecturer at the 14th International School on Rewriting, Obergurgl, Austria
• 4 April 2024: Translating HOL-Light proofs to Coq, 18 pages, 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 lambdapi, hol2dk and coq-hol-light
• 18 December 2023: new release of isabelle_dedukti
• 29 November - 7 December 2023: visit of Akihisa Yamada and Makoto Hamana within the Sakura project
• 8 September 2023: Invited talk on Progresses on proof system interoperability at CICM'23, Cambridge, UK
• 5 July 2023: Invited talk at the IFIP WG 1.6, Rome, Italy

Duties:

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