Dr. Hab. Frédéric BLANQUI INRIA permanent full-time researcher Project Deducteam Laboratoire Spécification et Vérification

Research interests: rewriting, type theory, λ-calculus, termination, logic, functional programming, proof assistants, ...

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

Internship/PhD/postdoc proposals:

• Advanced (co)induction in dependent type theory modulo rewriting (internship L3-M1-M2)
• Modern user interface for interactive theorem proving (internship L3-M1)
• Importing Agda proofs in Logipedia (internship L3-M1-M2)

News:

• 26 February 2020: deadline for submitting a workshop proposal for ICALP and LICS 2020
• 14 February 2020: The new rewriting engine of Dedukti, with Gabriel Hondet, 15 pages, submitted
• 13 February 2020: Type safety of rewriting rules in dependent types, 15 pages, submitted
• 23 July 2019: Ekstrakto: a tool to reconstruct Dedukti proofs from TSTP files, with Mohamed Yacine El Haddad and Guillaume Burel, 9 pages, PxTP'19
• 22 April 2019: Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, with Guillaume Genestier and Olivier Hermant, 21 pages, FSCD'19

Duties:

• Member of the scientific committee of Inria Paris-Saclay
• Deputy head of the pole C of the doctoral school STIC of the Université Paris-Saclay
• Workshop chair of the ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Member of the steering committees of ISR, TYPES and LICS
• PC member of the 6th International Conference on Formal Structures for Computation and Deduction (FSCD'21)
• PC member of the 13th Conference on Intelligent Computer Mathematics (CICM'20)
• PC member of the 15th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (LFMTP'20)
• PC member of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20)
• Organizer of the 11th International School on Rewriting (ISR'19) with Olivier Hermant
• PC member of the 16th International Colloquium on Theoretical Aspects of Computing (ICTAC'19)
• PC member of the 6th Workshop on Proof eXchange for Theorem Proving (PxTP'19)
• PC member of Large Mathematical Libraries (LML'19)

Teaching:

• Langages et Systèmes Formels à l'ENSIIE
• Rewriting Theory at the MPRI
• Préparation à l'agrégation à l'ENS Paris-Saclay

LSV, 61 avenue du Président Wilson, 94235 Cachan Cedex, France Office C1-09, Tel: +33 (0) 1 47 40 22 59, Fax: +33 (0) 1 47 40 75 21 Email: frederic . blanqui (a) inria . fr How to come?