View article

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 …