Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Wed 6 Sep 2017 11:37 - 12:00 at L1 - Dependently Typed Programming Chair(s): Dan Licata

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 natively implemented 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.

Wed 6 Sep
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

10:30 - 12:00: Research Papers - Dependently Typed Programming at L1
Chair(s): Dan LicataWesleyan University
icfp-2017-papers10:30 - 10:52
Stephanie WeirichUniversity of Pennsylvania, USA, Antoine VoizardUniversity of Pennsylvania, USA, Pedro Henrique Azevedo de AmorimEcole Polytechnique, n.n. / University of Campinas, Brazil, Richard A. EisenbergBryn Mawr College, USA
icfp-2017-papers10:52 - 11:15
Andreas NuytsKU Leuven, Belgium, Andrea VezzosiChalmers University of Technology, Sweden, Dominique DevrieseKU Leuven, Belgium
icfp-2017-papers11:15 - 11:37
Andreas AbelUniversity of Gothenburg, Sweden, Andrea VezzosiChalmers University of Technology, Sweden, Theo WinterhalterENS Paris-Saclay, France
icfp-2017-papers11:37 - 12:00
Gabriel EbnerVienna University of Technology, Austria, Sebastian UllrichKIT, Germany, Jared RoeschUniversity of Washington, USA, Jeremy AvigadCarnegie Mellon University, USA, Leonardo De MouraMicrosoft Research, n.n.