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

The de~Bruijn representation of syntax with binding is commonly used, but flawed when it comes to recursion. As the structural recursion principle associated to an inductive type of expressions is unaware of the binding discipline, each recursive definition requires a separate proof of compatibility with variable instantiation. We solve this problem by extending Allais' notion of syntax traversals to obtain a framework for instantiation-compatible recursion. The framework is general enough to handle multivariate, potentially mutually recursive syntactic systems.

With our framework we define variable renaming and instantiation, syntax directed typing and certain unary logical relations for System~F. These definitons lead to concise proofs of type preservation, as well as weak and strong normalisation.

Our framework is designed to serve as the theoretical foundation of future versions of the Autosubst Coq library. All developments and case studies are formalised in the Coq proof assistant.

Tue 9 Jan

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