Metaprogramming with Dependent Type Theory

1 hour 7 mins, 971.73 MB, MPEG-4 Video 640x360, 29.97 fps, 44100 Hz, 1.93 Mbits/sec

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/2525417/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	De Moura, L Wednesday 12th July 2017 - 10:00 to 11:00


Created:	2017-07-26 13:21
Collection:	Big proof
Publisher:	Isaac Newton Institute
Copyright:	De Moura, L
Language:	eng (English)
Distribution:	World (downloadable)
Explicit content:	No
Aspect Ratio:	16:9
Screencast:	No
Bumper:	UCS Default
Trailer:	UCS Default


Abstract:	Co-authors: Gabriel Ebner (Vienna University of Technology), Sebastian Ullrich (Karlsruhe Institute of Technology), Jared Roesch (University of Washington), Jeremy Avigad (Carnegie Mellon University) Dependent type theory is a powerful framework for interactive theorem proving and automated reasoning, allowing us to encode mathematical objects, data type specifications, assertions, proofs, and programs, all in the same language. Here we show that dependent type theory can also serve as its own metaprogramming language, that is, a language in which one can write programs that assist in the construction and manipulation of terms in dependent type theory itself. Specifically, we describe the metaprogramming language currently in use in the Lean theorem prover, which extends Lean's object language with an API for accessing internal procedures and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our language is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation. Related Links https://leanprover.github.io/ - Lean website

Abstract:

Co-authors: Gabriel Ebner (Vienna University of Technology), Sebastian Ullrich (Karlsruhe Institute of Technology), Jared Roesch (University of Washington), Jeremy Avigad (Carnegie Mellon University)

Dependent type theory is a powerful framework for interactive theorem proving and automated reasoning, allowing us to encode mathematical objects, data type specifications, assertions, proofs, and programs, all in the same language. Here we show that dependent type theory can also serve as its own metaprogramming language, that is, a language in which one can write programs that assist in the construction and manipulation of terms in dependent type theory itself. Specifically, we describe the metaprogramming language currently in use in the Lean theorem prover, which extends Lean's object language with an API for accessing internal procedures and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our language is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation.

Related Links
https://leanprover.github.io/ - Lean website

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video *	640x360	1.93 Mbits/sec	971.73 MB	View	Download
WebM	640x360	484.86 kbits/sec	237.93 MB	View	Download
iPod Video	480x270	524.48 kbits/sec	257.38 MB	View	Download
MP3	44100 Hz	251.19 kbits/sec	123.27 MB	Listen	Download
Auto	(Allows browser to choose a format it supports)

Streaming Media Service Upload

Metaprogramming with Dependent Type Theory