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:
News:
- 4 February 2025: new release of lambdapi and lambdapi-stdlib
- 17 December 2024: complete translation of HOL-Light base library in Coq
- 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: 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
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 |
![[logo ENS Paris-Saclay]](img/logo_ens_paris_saclay.png) |
Last updated on 11 February 2025.
Come back to main page.