Dr. Hab. Frédéric BLANQUI Research director at Inria Project Deducteam Chair of EuroProofNet

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

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

Internship/PhD/postdoc proposals:

• Certifying PVS proofs
• Generating Dedukti proofs from SMT solver proofs
• Inter-system translation of recursive functions
• Integrating and reusing Dedukti proofs in other provers

News:

• 25 August - 1st September 2024: Invited lecturer at the 14th International School on Rewriting, Obergurgl, Austria
• 8 September 2023: Invited talk on Progresses on proof system interoperability at CICM'23, Cambridge, UK
• 30 August 2023: Sharing proofs with predicative theories through universe polymorphic elaboration, with Thiago Felicissimo, 36 pages, submitted
• 31 July 2023: Release of Lambdapi 2.4.0
• 5 July 2023: Invited talk at the IFIP WG 1.6, Rome, Italy
• 2 July 2023: 18th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (LFMTP'23), Rome, Italy
• May 30-June 10: I am visiting Akihisa Yamada, Jérémy Dubut and Makoto Hamana (Sakura project)
• 14 February 2023: A modular construction of type theories, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 28 pages, published in LMCS
• 13 February 2023: Translating proofs from an impredicative type system to a predicative one, with Thiago Felicissimo and Ashish Kumar Barnawal, 19 pages, CSL'23
• 30 January 2023: new translator from HOL-Light to Dedukti and Lambdapi, and Coq
• 27-29 January 2023: 2nd Dedukti tools developers meeting
• 27 September 2022: PhD defense of Gabriel Hondet on Expressing predicate subtyping in computational logical frameworks
• 23-24 September 2022: EuroProofNet Workshop on the development, maintenance, refactoring and search of large libraries of proofs
• 6 May 2022: L’interopérabilité des systèmes de preuve, post dans le blog Binaire sur Lemonde.fr
• 19 April 2022: Encoding type universes without using matching modulo AC, 14 pages, FSCD'22
• 9 March 2022: Proof systems: strengthening the position of the EU through EuroProofNet

Duties:

• Chair of the European COST action CA20111 EuroProofNet (>320 participants from 42 countries)
• French PI of a Sakura 2022-2023 project with Japan
• 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 committee of ISR

LMF, 4 avenue des Sciences, 91190 Gif-sur-Yvette, France Office 3U61, Tel: +33 (0) 1 81 87 54 35 Email: frederic . blanqui (a) inria . fr How to come? Transport - Campus