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:

• CDD 3 ans ingénieur Inria pour aider dans le test, la maintenance et le développement d'outils pour l'interopérabilité entre systèmes de preuves (intégration continue, gestionnaire de bibliothèques de preuves, algorithmes de recherche, VSCode, etc.)! Salaire mensuel net entre 2148 et 4412 euros selon expérience. Envoyez-moi votre CV.
• 3-years engineer contract at Inria to help develop, test and maintain tools for proof system interoperability (continuous integration, packages management, search tools, VSCode, etc.)! Net taxable monthly salary between 2148 and 4412 euros depending on experience, including social security and 9 weeks holidays/year. Send me your CV.

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