Tue 9 Jan 2018 16:30 - 17:00 at Museum A - Formalizing Meta-Theory Chair(s): Brigitte Pientka

We present a Coq formalization of the normalization-by-evaluation algorithm for Martin-Löf dependent type theory with one universe and judgmental equality. The end results of the formalization are certified implementations of a reduction-free normalizer and of a decision procedure for term equality.

The formalization takes advantage of a graph-based variant of the Bove-Capretta method to encode mutually recursive evaluation functions with nested recursive calls. The proof of completeness, which uses the PER-model of dependent types, is formalized by relying on impredicativity of the Coq system rather than on the commonly used induction-recursion scheme which is not available in Coq. The proof of soundness is formalized by encoding logical relations as partial functions.

Tue 9 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

CPP-2018
16:00 - 18:00: CPP 2018 - Formalizing Meta-Theory at Museum A
Chair(s): Brigitte PientkaMcGill University
CPP-201816:00 - 16:30
Talk
Sergueï LengletUniversity of Lorraine, France, Alan SchmittInria
DOI
CPP-201816:30 - 17:00
Talk
Paweł WieczorekUniversity of Wrocław, Dariusz BiernackiUniversity of Wrocław
DOI
CPP-201817:00 - 17:30
Talk
Kaustuv ChaudhuriInria, France
DOI
CPP-201817:30 - 18:00
Talk
Jonas Kaiser, Steven Schäfer, Kathrin StarkSaarland University, Germany
DOI