Dr. Hab. Frédéric BLANQUI INRIA permanent full-time researcher Project Deducteam Laboratoire Méthodes Formelles

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

Publications  | Talks  | Software  | Teaching  | Students  | Useful links  | Homepages  | PC

Internship/PhD/postdoc proposals:

• Developping a standard library for Lambdapi (L3-M1)

News:

• 3 November 2021: Encoding type universes without using matching modulo AC, 15 pages, draft
• 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 (200 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

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