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

Lambda-tree syntax (λTS), also known as higher-order abstract syntax (HOAS), is a representational technique where the pure λ-calculus in a meta-language is used to represent binding constructs in an object language. A key feature of λTS is that capture-avoiding substitution in the object language is represented by β-reduction in the meta language. However, to reason about the meta-theory of (simultaneous) substitutions, it may seem that λTS gets in the way: not only does iterated β-reduction not capture simultaneity, but also β-redexes are not first-class constructs.

This paper proposes a representation of (simultaneous) substitutions in the two-level logic approach (2LLA), where properties of a specification language are established in a strong reasoning meta-logic that supports inductive reasoning. A substitution, which is a partial map from variables to terms, is represented in a form similar to typing contexts, which are partial maps from variables to types; both are first-class in 2LLA. The standard typing rules for substitutions are then just a kind of context relation that are already well-known in 2LLA. This representation neither changes the reasoning kernel, nor requires any modification of existing type systems, and does not sacrifice any expressivity.

Tue 9 Jan (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