Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 11:00 - 11:30 at Sala XII - Research Papers: Rewriting, Automated Reasoning Chair(s): Andrei Popescu

Formalising metatheory in the Coq proof assistant is tedious as native support for reasoning with binders requires a lot of uninteresting technicalities. To relieve users from so-produced boilerplate, the Autosubst framework automates working with de Bruijn terms: For each annotated inductive type, Autosubst generates a corresponding instantiation operation for parallel substitutions and a decision procedure for assumption-free substitution lemmas. However, Autosubst is implemented in Ltac, Coq’s tactic language, and thus suffers from Ltac’s limitations. In particular, Autosubst is restricted to Coq and unscoped, non-mutual inductive types with a single sort of variables. In this paper, we present a new version of Autosubst that overcomes these restrictions. Autosubst 2 is an external code generator, which translates second-order HOAS specifications into potentially mutual inductive term sorts. We extend the equational theory of Autosubst to the case of mutual inductive sorts by combining the application of multiple parallel substitutions into exactly one instantiation operation for each sort, i.e. we parallelise substitutions to vector substitutions. The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework and allows us to present an even more elegant proof for the POPLMark challenge.

Tue 15 Jan

CPP-2019
11:00 - 12:30: CPP 2019 - Research Papers: Rewriting, Automated Reasoning at Sala XII
Chair(s): Andrei PopescuMiddlesex University, London
CPP-201911:00 - 11:30
Research paper
Kathrin StarkSaarland University, Germany, Steven SchäferSaarland University, Jonas Kaiser
DOI
CPP-201911:30 - 12:00
Research paper
Alexander Lochmann, Christian SternagelUniversity of Innsbruck, Austria
DOI
CPP-201912:00 - 12:30
Research paper
DOI