BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Metaprogramming with Dependent Type Theory - Leonardo de Moura (Mi
 crosoft (UK))
DTSTART:20170712T090000Z
DTEND:20170712T100000Z
UID:TALK73254@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:<span>Co-authors: Gabriel Ebner		(Vienna University of Technol
 ogy)\, Sebastian Ullrich		(Karlsruhe Institute of Technology)\, Jared Roes
 ch		(University of Washington)\, Jeremy Avigad		(Carnegie Mellon Universit
 y)        <br></span><br>Dependent type theory is a powerful framework for
  interactive theorem proving and automated reasoning\, allowing us to enco
 de mathematical objects\, data type specifications\, assertions\, proofs\,
  and programs\, all in the same language.  Here we show that dependent typ
 e theory can also serve as its own metaprogramming language\, that is\, a 
 language in which one can write programs that assist in the construction a
 nd manipulation of terms in dependent type theory itself. Specifically\, w
 e describe the metaprogramming language currently in use in the Lean theor
 em prover\, which extends Lean&#39\;s object language with an API for acce
 ssing internal procedures and provides ways of reflecting object-level exp
 ressions into the metalanguage. We provide evidence to show that our langu
 age is performant\, and that it provides a convenient and flexible way of 
 writing not only small-scale interactive tactics\, but also more substanti
 al kinds of automation. <br><br>Related Links<ul><li><a target="_blank" re
 l="nofollow" href="http://www-old.newton.ac.uk/cgi/https%3A%2F%2Fleanprove
 r.github.io%2F">https://leanprover.github.io/</a> - Lean website</li></ul>
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR