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:

• Structured proofs in Lambdapi (L3-M1)
• Importing Logipedia proofs in Agda (M1-M2)
• Developping a standard library for Lambdapi (L3-M1)
• Encoding Agda and coinduction in Dedukti (M1-M2)
• Translating Isabelle proofs to Dedukti (M1-M2)

News:

• 3 May 2021: Some axioms for mathematics, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 18 pages, to appear in the proceedings of FSCD'21
• 19 February 2021: Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-calculus Modulo Theory, with Gabriel Hondet, 18 pages, to appear in the post-proceedings of TYPES'20

EuroProofNet:

EuroProofNet is an European COST action aiming at boosting the interoperability and usability of proof systems and making formal proofs enter a new era. For the first time, it gathers all the developers and users of proof systems in Europe. To make their proofs exchangeable, they will express the logical foundations of their systems in a common logical framework, and develop tools for the inter-translation of the proofs developed in individual systems to and from this common logical framework.

The project will start in October 2021.

Anyone from a participating country can ask fundings for short-term scientific missions in the network, especially young researchers, female researchers or researchers from inclusive target countries. More details will be given in the coming months.

24 countries are currently participating: Austria, Belgium, Bulgaria, Croatia, Czech Republic, Denmark, Estonia, France, Germany, Hungary, Iceland, Italy, Luxembourg, Netherlands, North Macedonia, Norway, Poland, Portugal, Romania, Serbia, Slovenia, Spain, Sweden, United Kingdom.

Duties:

• Coordinator of the European COST project EuroProofNet
• Assistant director of the Paris-Saclay doctoral school of computer science in charge of the budget
• 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 13th Conference on Intelligent Computer Mathematics (CICM'21)
• PC member of the 27th International Conference on Types for Proofs and Programs (TYPES'21)

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