Dr. Hab. Frédéric BLANQUI Research director Project Deducteam Laboratoire Méthodes Formelles

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
• Translating Lean to Dedukti

News:

• 1 October 2022: Translating proofs from an impredicative type system to a predicative one, with Thiago Felicissimo and Ashish Kumar Barnawal, 20 pages, accepted to CSL'23
• 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
• 14 July 2022: Some axioms for type systems, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 28 pages, to appear in LMCS
• 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, accepted at FSCD'22
• 18 March 2022: Release of Lambdapi 2.2.0 (includes an incremental local confluence checker)
• 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 (~300 participants from 40 countries)
• Co-leader 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 committees of ISR and LICS
• Workshop chair of the ACM/IEEE Symposium on Logic in Computer Science (LICS)
• PC member of the 11th International Joint Conference on Automated Reasoning (IJCAR'22)
• PC member of the 28th International Conference on Types for Proofs and Programs (TYPES'22)

Teaching:

• Langages et Systèmes Formels à l'ENSIIE
• Rewriting Theory at the MPRI

LMF, 4 avenue des Sciences, 91190 Gif-sur-Yvette, France Office 3S61, Tel: +33 (0) 1 81 87 54 35 Email: frederic . blanqui (a) inria . fr How to come? Transport - Campus