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

  Browse A-Z

Log in

Cambridge users (raven)details Other usersdetails No account?details

Information on

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

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.

Other lists

MRC Biostatistics Unit Centenary Events Babbage Seminar Series The obesity epidemic: Discussing the global health crisis Abcam meetings Oliver Wyman lecture : "The economic outlook: The news behind the headlines" Representational Similarity Analysis

Other talks

An investigation into hepatocyte expression and prognostic significance of senescence marker p21 in canine chronic hepatitis How archaeologists resolve the inductive risk argument The Knotty Maths of Medicine Sustainability 101: how to frame it, change it and steer it Measuring interacting electrons in low dimensional systems: spin-charge separation and 'replicas & tbd Bayesian deep learning
 

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