Steven Keuchel, Tom Schrijvers and Stephanie Weirich.
Submitted to the 26th European Symposium on Programming (ESOP'17), 2017.
Many approaches have been developed that tackle the substantial boilerplate that arises from variable binding in programming language mechanizations. Unfortunately, existing approaches for first-order representations are limited to reasoning about the interactions between syntactic operations such as substitution and free variable calculation, and are no help for lemmas that describe the interactions between syntactic operations and relations. For example, lemmas stating that substitution preserves typing must be proven manually.
We address this issue by extending the Knot specification language with definitions of relations on top of the existing support for syntactic sorts. The language ensures that the expressions that appear in these relations are well-scoped and makes explicit where terms cross binders to avoid capture. We also extend Knot's code generator Needle to produce specialized Coq definitions, including boilerplate such as well-scopedness, weakening and substitution lemmas for relations.
Our evaluation shows on average 71% savings in comparison to fully manual Coq mechanizations and 33% to the previous Needle version without support for relations in a case-study of type-safety mechanizations for 11 languages. In particular we set a new record for the POPLmark challenge (1a + 2a) by providing a solution in under 200 lines of code.
The tarball contains the Needle code generator as well as the code for the case studies.
Steven Keuchel, Stephanie Weirich and Tom Schrijvers.
Submitted to the 25th European Symposium on Programming (ESOP'16), 2016.
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 extends the support for binder boilerplate. Knot is a highly expressive language for natural and concise specification of syntax with binders. Its meta-theory 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 size of language mechanizations (by 40% in our case study). Moreover, as far as we know, Knot enables the most concise mechanization of the POPLmark Challenge (1a + 2a) and is two-thirds the size of the next smallest. 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.
The tarball contains the generic implementation, the Needle code generator as well as the code for both case studies. Update Oct 29th:The version of Needle at submission time does not compile under GHC 7.6 and two module names are off due to developing under OS X with a case-insensitive filesystem. This has been fixed and an updated tarball can be found here.
Ongoing development of Needle can be found on our GitHub project page.