Frédéric Blanqui's homepage

Dr. Hab. Frédéric BLANQUI

INRIA permanent full-time researcher

Research interests: rewriting, type theory, λ-calculus, termination, proof assistants, proof system interoperability, ...

Internship/PhD/postdoc proposals:

Term transformation and proof (re)construction (L3-M2)
Translating Lean to Dedukti (M1-M2)
Developping a standard library for Lambdapi (L3-M1)

News:

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, 15 pages, accepted at FSCD'20
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
28 February 2022: Sakura 2022-2023 project with Japan accepted
25 January 2022: Lambdapi used in Quentin Garchery's PhD work!
31 October 2021: Some axioms for mathematics, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 27 pages, submitted to LMCS

Duties:

Chair of the European COST action CA20111 EuroProofNet (>240 participants from 30 countries)
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, TYPES 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

Address:

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

Last updated on 18 May 2022. Come back to main page.