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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

The Lean HoTT library

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

to be confirmed Part II room, Department of Genetics. Please use the entrance by the Part II room and tea room underneath the external fire escape. Main entrance is not connected to Part II room due to refurbishment. Hodgkin-Huxley Seminar Room Department of Physiology, Development & Neuroscience

Other talks

Online Causal Inference Seminar Morning Break A scientists guide to the art of radiation therapy and Neurosurgery for the oncologist Fun experiments you can only do with frogs Reproducibility In Astrophysical Simulations: The AGORA Initiative and a 14-Year Human Experiment (In Memory of Joel Primack) Group Work
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity