Mechanising Syntax with Binders in Coq
Author: Kathrin Stark
Supervisor: Prof. Dr. Gert Smolka
Status: Submitted on December 11, 2019; colloquium held on February 14, 2020
Abstract
Mechanising binders in general-purpose proof assistants such as Coq is cumbersome and difficult.
Yet binders, substitutions, and instantiation of terms with substitutions are a critical ingredient of many programming languages. Any practicable mechanisation of the meta-theory of the latter hence
requires a lean formalisation of the former.
We investigate the topic from three angles:
First, we realise formal systems with binders based on both pure and scoped de Bruijn algebras together with basic syntactic rewriting lemmas and automation. We automate this process in a compiler called Autosubst; our final tool supports many-sorted, variadic, and modular syntax.
Second, we justify our choice of realisation and mechanise a proof of convergence of the sigma calculus, a calculus of explicit substitutions that is complete for equality of the de Bruijn algebra corresponding to the lambda calculus.
Third, to demonstrate the practical usefulness of our approach, we provide concise, transparent, and accessible mechanised proofs for a variety of case studies refined to de Bruijn substitutions.
Documents
Formalisations
You can find the Autosubst 2 compiler here.
