View article

This extended abstract showcases NEEDLE & KNOT, a framework for programming language mechanization. Our framework tackles the problem that formal proofs about programming language semantics and type-systems are long and error-prone. To guarantee their correctness, techniques for mechanical formalization in proof assistants, such as ones based on type-theories, have received much attention in recent years. However, human mechanizers of programming language meta-theory are unnecessarily burdened with boilerplate that arises from variable bindings in programming languages. To tackle the substantial boilerplate for richer languages, support from the proof assistant or from tools is mandatory. NEEDLE & KNOT specifically target the boilerplate that arises in type-safety proofs of typed programming languages. In particular, they use the syntactic approach to programming language metatheory, invented by Wright and Felleisen [13] and popularized by Pierce [10]. The treatment of variable binding typically comprises the better part of such formalizations. Most of this variable binding infrastructure is repetitive and tedious boilerplate. By boilerplate we mean mechanical operations and lemmas that appear in many languages, such as: 1) common operations like calculating the sets of free variables or the domain of a typing context, appending contexts and substitutions; 2) lemmas about operations like commutation of substitutions or the interaction between the free-variable calculation and substitution; and 3) lemmas about semantic relations such as the preservation of well-scoping and typing under operations.

Our approach …