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, Goiânia, Brazil
- 25 August - 1st September 2024: Invited lecturer at the 14th International School on Rewriting, Obergurgl, Austria
- 4 April 2024: Translating HOL-Light proofs to Coq, 18 pages, 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 lambdapi, 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
- 8 September 2023: Invited talk on Progresses on proof system interoperability at CICM'23, Cambridge, UK
- 5 July 2023: Invited talk at the IFIP WG 1.6, Rome, Italy
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 17 April 2024.
Come back to main page.