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

Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics.

In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier $\forall$ which lets us ignore sizes in terms for equality checking, alongside with a second quantifier $\Pi$ for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features \emph{type shape}-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.

Wed 6 Sep

Displayed time zone: Belfast change

10:30 - 12:00
Dependently Typed ProgrammingResearch Papers at L1
Chair(s): Daniel R. 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, Théo 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