<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div><div>He mentions CakeML around minute 34 to 35 in the video.</div><div><br></div><div>-Scott</div><div><br></div><div>On 2014/06/25, at 12:46, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html; charset=utf-8"><div dir="ltr">In the PDF below Hales makes some nice mentions of CakeML :)<br><div><br><div class="gmail_quote">---------- Forwarded message ----------<br>From: <b class="gmail_sendername">Josef Urban</b> <span dir="ltr"><<a href="mailto:josef.urban@gmail.com">josef.urban@gmail.com</a>></span><br>

Date: Wed, Jun 25, 2014 at 12:34 PM<br>Subject: [Coq-Club] Tom Hales on Formal proof at the Bourbaki seminar<br>To: mizar-forum <<a href="mailto:mizar-forum@mizar.uwb.edu.pl">mizar-forum@mizar.uwb.edu.pl</a>>, isabelle-users <<a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>>, hol-info <<a href="mailto:hol-info@lists.sourceforge.net">hol-info@lists.sourceforge.net</a>>, coq-club <<a href="mailto:coq-club@inria.fr">coq-club@inria.fr</a>>, Foundations of Mathematics <<a href="mailto:fom@cs.nyu.edu">fom@cs.nyu.edu</a>>, projects-mkm-ig <<a href="mailto:projects-mkm-ig@lists.jacobs-university.de">projects-mkm-ig@lists.jacobs-university.de</a>><br>

<br><br><a href="http://www.bourbaki.ens.fr/TEXTES/1086.pdf" target="_blank">http://www.bourbaki.ens.fr/TEXTES/1086.pdf</a><br>
<br>
The whole session is here (with video links):<br>
<a href="http://www.bourbaki.ens.fr/seminaires/2014/Prog_juin14.html" target="_blank">http://www.bourbaki.ens.fr/seminaires/2014/Prog_juin14.html</a><br>
<span class="HOEnZb"><font color="#888888"><br>
Josef<br>
</font></span></div><br></div></div>
_______________________________________________<br>Users mailing list<br><a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>https://lists.cakeml.org/listinfo/users<br></blockquote></div><br></body></html>