Research interests: proof system interoperability,
proof assistants, rewriting, type theory, λ-calculus, termination,
| Useful links
- 2 July 2023: 18th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (LFMTP'23), Rome, Italy
- 4 January 2023: Release of Lambdapi 2.3.0
- 1st December 2022: A modular construction of type theories, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 28 pages, to appear in LMCS
- 14 November 2022: Translating proofs from an impredicative type system to a predicative one, with Thiago Felicissimo and Ashish Kumar Barnawal, 19 pages, CSL'23
- 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
- 5-9 September 2022: See my lectures on proof system interoperability at the VTSA'22, Saarbrücken, Germany
- 24-25 June 2022: 1st Dedukti School [slides] [video]
- 23 May 2022: Visit Akihisa Yamada in Tokyo and Makoto Hamana in Kiryu
- 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
- 25 January 2022: Lambdapi used in Quentin Garchery's PhD work!
|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?
Last updated on 1 February 2023.
Come back to main page.