University of Cambridge > > Isaac Newton Institute Seminar Series > The Lean HoTT library

The Lean HoTT library

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact INI IT.

BPR - Big proof

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.

This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity