Publication details

Saarland University Computer Science

Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions

Kathrin Stark, Steven Schäfer, Jonas Kaiser

8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, 2019

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.

Download PDF        Show BibTeX        Download slides (PDF)       

Login to edit

Legal notice, Privacy policy