Needle Knot: Binder boilerplate tied up

摘要

In order to lighten the burden of programming language mechanization many approaches have been developed that tackle the substantial boilerplate which arises from variable binders. Unfortunately,the existing approaches are limited in scope. They typically do not support complex binding forms (such as multi-binders) that arise in more advanced languages, or they do not tackle the boilerplate due to mentioning variables and binders in relations. As a consequence, the human mechanizer is still unnecessarily burdened with binder boilerplate and discouraged from taking on richer languages.This paper presents Knot, a new approach that substantially extendsthe support for binder boilerplate. Knot is a highly expressive languagefor natural and concise specification of syntax with binders. Its metatheory constructively guarantees for well-formed specifications the coverage of a considerable amount of binder boilerplate, including that for well-scoping of terms and context lookups. Knot also comes with a code generator, Needle, that specializes the generic boilerplate for convenient embedding in Coq and provides a tactic library for automatically discharging proof obligations that frequently come up in proofs of weakening and substitution lemmas of type-systems.Our evaluation shows, that Needle & Knot significantly reduce the sizeof language mechanizations (by 40% in our case study). Moreover, asfar as we know, Knot enables the most concise mechanization of thePOPLmark Challenge (1a + 2a) and is two-thirds the size of the nextsmallest. Finally, Knot allows us to mechanize for instance dependently-typed languages, which is notoriously challenging because of dependent contexts and mutually-recursive sorts with variables.