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:
18-20 September 2024: 19th Logical and Semantic Frameworks with Applications (LSFA'24), Goiânia, Brazil
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
18 December 2023: new release of isabelle_dedukti
29 November - 7 December 2023: visit of Akihisa Yamada and Makoto Hamana within the Sakura project
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 25 September 2024.
Come back to main page .