BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Lean Theorem Prover - Jeremy Avigad (Carnegie Mellon Universit
 y)
DTSTART:20170629T100000Z
DTEND:20170629T110000Z
UID:TALK73112@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Lean is a new\, open source\, interactive theorem prover&nbsp\
 ;designed to<br>support mathematical reasoning as well as hardware and sof
 tware<br>verification. Because its logical foundation\,&nbsp\;dependent<br
 >type theory\, has a computational interpretation\, we&nbsp\;can use Lean<
 br>as a programming language and evaluate expressions&nbsp\;with a fast<br
 >bytecode evaluator. We obtain a metaprogramming language --<br>that is\, 
 a language that we can use to construct expressions<br>and proofs in depen
 dent type theory itself -- by&nbsp\;exposing Lean<br>internals through a s
 uitable API. This provides us with a means<br>of extending Lean&#39\;s fun
 ctionality and automation within Lean<br>itself. In this talk\, I will des
 cribe this<br>metaprogramming framework and some of its mechanisms for&nbs
 p\;manipulating<br>expressions efficiently.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR