Research interests: proof system interoperability,
proof assistants, rewriting, type theory, λ-calculus, termination,
...
Publications
| Talks
| Software
| Teaching
| Students
| Useful links
| Homepages
| PC
News:
- 13 September 2024: Translating libraries of definitions and theorems between proof systems (invited talk), 15th International Conference on Interactive Theorem Proving, (ITP'24) , Tbilisi, Georgia
- 13-14 September 2024: EuroProofNet WG4 meeting on proof libraries, Tbilisi, Georgia
- 25 August - 1st September 2024: Invited lecturer at the 14th International School on Rewriting, Obergurgl, Austria
- 29 July 2024: new release of lambdapi
- 29 July 2024: talk on Translating HOL-Light proofs to Coq, Workshop on Libraries of Digital Math, Trimester Program: "Prospects of Formal Mathematics", Hausdorff Institute for Mathematics, Bonn, Germany [video]
- 4 April 2024: Translating HOL-Light proofs to Coq, accepted at LPAR'24
- 5 March 2024: new version of Sharing proofs with predicative theories through universe polymorphic elaboration, with Thiago Felicissimo, 38 pages, accepted for publication in LMCS
- 26 February 2024: new releases of hol2dk and coq-hol-light
Duties:
Address:
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 |
|
Last updated on 18 November 2024.
Come back to main page.