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:

• Modern user interface for interactive theorem proving (L3, M1 or M2)
• Checking the type safety of rewrite rules (M1 or M2)
• Efficient rewriting modulo associativity and commutativity (M1 or M2)

Teaching:

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

Duties:

• Deputy head of the pole 4 of the doctoral school STIC of the University Paris-Saclay
• Workshop chair of LICS
• Member of the steering committee of the International School on Rewriting (ISR)
• 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 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20)

News:

• 17 November 2018: Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, with Guillaume Genestier and Olivier Hermant, 23 pages, 2018, submitted to FOSSACS 2019
• 8 October 2018: List of lecturers of the 11th International School on Rewriting (ISR'19), Ecole des Mines, Paris
• 4 July 2018: Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'18), EPTCS 274, with Giselle Reis
• 15 June 2018: Works in progress and experience reports of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'18), with Giselle Reis
• 11 June 2018: Termination of λΠ modulo rewriting using the size-change principle (work in progress), with Guillaume Genestier, 5 pages, WST'18
• 4 May 2018: release of CoLoR 1.5 for Coq 8.8
• 21 April 2018: Size-based termination of higher-order rewriting, published in JFP
• 5 March 2018: Note on the operational semantics of Dedukti 2.5

Events:

• 30 October - 6 November 2019: 16th International Colloquium on Theoretical Aspects of Computing (ICTAC'19), Hammamet, Tunisia
• 1-6 July 2019: 11th International School on Rewriting (ISR'19), Ecole des Mines, Paris
• 22-27 June 2019: 34th ACM/IEEE Symposium on Logic in Computer Science (LICS), Vancouver, Canada
• 9 October 2018: Upscale meeting

Address:

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?