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

Displayed time zone: Belfast change

10:30 - 12:00
Dependently Typed ProgrammingResearch Papers at L1
Chair(s): Dan Licata Wesleyan University
10:30
22m
Talk
A Specification for Dependent Types in Haskell
Research Papers
Stephanie Weirich University of Pennsylvania, USA, Antoine Voizard University of Pennsylvania, USA, Pedro Henrique Azevedo de Amorim Ecole Polytechnique, n.n. / University of Campinas, Brazil, Richard A. Eisenberg Bryn Mawr College, USA
DOI
10:52
22m
Talk
Parametric Quantifiers for Dependent Type Theory
Research Papers
Andreas Nuyts KU Leuven, Belgium, Andrea Vezzosi Chalmers University of Technology, Sweden, Dominique Devriese KU Leuven, Belgium
DOI
11:15
22m
Talk
Normalization by Evaluation for Sized Dependent Types
Research Papers
Andreas Abel University of Gothenburg, Sweden, Andrea Vezzosi Chalmers University of Technology, Sweden, Theo Winterhalter ENS Paris-Saclay, France
DOI
11:37
22m
Talk
A Metaprogramming Framework for Formal Verification
Research Papers
Gabriel Ebner Vienna University of Technology, Austria, Sebastian Ullrich KIT, Germany, Jared Roesch University of Washington, USA, Jeremy Avigad Carnegie Mellon University, USA, Leonardo de Moura Microsoft Research, n.n.
DOI