skip to content

The Lean HoTT library

Presented by: 
Floris van Doorn Carnegie Mellon University
Friday 7th July 2017 - 11:30 to 12:00
INI Seminar Room 2
An overview of the homotopy type theory library in Lean, in comparison towards the other proof assistants available for HoTT. This talk is more aimed towards the HoTT community. A second talk will be given during the workshop which is more aimed towards the formal verification community.

[ The video of this talk is temporarily unavailable. Please try later. ]

Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons