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

Job offer:

• Je cherche un programmeur pour développer un gestionnaire de paquets pour des fichiers de preuves. Salaire net entre 2148 et 4412 euros selon expérience.

Internship/PhD/postdoc proposals:

• Certifying PVS proofs
• Generating Dedukti proofs from SMT solver proofs
• Translating Lean to Dedukti
• Inter-system translation of recursive functions
• Integrating and reusing Dedukti proofs in other provers

News:

• 2 July 2023: 18th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (LFMTP'23), Rome, Italy
• 30 January 2023: new translator from HOL-Light to Dedukti and Lambdapi
• 27-29 January 2023: 2nd Dedukti tools developers meeting
• 4 January 2023: Release of Lambdapi 2.3.0
• 1st December 2022: A modular construction of type theories, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 28 pages, to appear in LMCS
• 14 November 2022: Translating proofs from an impredicative type system to a predicative one, with Thiago Felicissimo and Ashish Kumar Barnawal, 19 pages, CSL'23
• 27 September 2022: PhD defense of Gabriel Hondet on Expressing predicate subtyping in computational logical frameworks
• 23-24 September 2022: EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs
• 5-9 September 2022: See my lectures on proof system interoperability at the VTSA'22, Saarbrücken, Germany
• 24-25 June 2022: 1st Dedukti School [slides] [video]
• 23 May 2022: Visit Akihisa Yamada in Tokyo and Makoto Hamana in Kiryu
• 6 May 2022: L’interopérabilité des systèmes de preuve, post dans le blog Binaire sur Lemonde.fr
• 19 April 2022: Encoding type universes without using matching modulo AC, 14 pages, FSCD'22
• 9 March 2022: Proof systems: strengthening the position of the EU through EuroProofNet
• 25 January 2022: Lambdapi used in Quentin Garchery's PhD work!

Duties:

• Chair of the European COST action CA20111 EuroProofNet (>320 participants from 42 countries)
• French PI of a Sakura 2022-2023 project with Japan
• Assistant director of the Paris-Saclay doctoral school of computer science in charge of the budget
• Member of the evaluation committee of Inria
• Member of the scientific committee of Inria Paris-Saclay
• Member of the steering committee of ISR

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