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, proof assistants, ...

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

Internship/PhD/postdoc proposals:

• Structured proofs in Dedukti (internship L3-M1-M2)

News:

• 1st November 2020: Encoding of Predicate Subtyping and Proof Irrelevance in the λΠ-calculus Modulo Theory, with Gabriel Hondet, 18 pages, submitted
• 19 May 2020: moving to the new ENS campus, 4 avenue des Sciences, 91190 Gif-sur-Yvette, France
• 25 April 2020: The new rewriting engine of Dedukti, with Gabriel Hondet, 16 pages, accepted at FSCD'20
• 25 April 2020: Type safety of rewrite rules in dependent types, 15 pages, accepted at FSCD'20

Duties:

• 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 6th International Conference on Formal Structures for Computation and Deduction (FSCD'21)
• PC member of the 17th International Colloquium on Theoretical Aspects of Computing (ICTAC'20)
• PC member of the 13th Conference on Intelligent Computer Mathematics (CICM'20)
• Member of the panel of the 9th Confluence Competition (CoCo'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)

Teaching:

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

LSV, 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