University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Why you can't even trust HOL, and what to do about it

  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

Why you can't even trust HOL, and what to do about it

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

If you have a question about this talk, please contact Thomas Tuerk.

In this talk, I will expose various problems in using existing HOL theorem provers, and advocate the use of a new proof-checker for HOL that is carefully designed to avoid these problems.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Annual Disability Lecture Cambridge Review of International Affairs Occasional Nuclear Energy Seminars

Other talks

Lunchtime Talk: Helen's Bedroom Brest-Litovsk and the Making of Modern Ukraine and Russia Kiwi Scientific Acceleration on FPGA Academic CV Workshop Cafe Synthetique: Synthetic Biology Industry Night Simulating wave propagation in elastic systems using the Finite-Difference-Time-Domain method "The integrated stress response – a double edged sword in skeletal development and disease" An SU(3) variant of instanton homology for webs The Anne McLaren Lecture: CRISPR-Cas Gene Editing: Biology, Technology and Ethics Protein Folding, Evolution and Interactions Symposium 'The Japanese Mingei Movement and the art of Katazome' The Deciding Factor - An afternoon talk
 

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