A Modular Approach to Metatheoretic Reasoning for Extensible Languages

This article concerns the development of metatheory for extensible languages. It starts with the view that programming languages tailored to specific application domains are to be constructed by composing components from an open library of independently-developed extensions to a host language. In this context, static analyses (such as typing) and dynamic semantics (such as evaluation) are described via relations whose specifications are distributed across the host language and extensions and are given in a rule-based fashion. Metatheoretic properties, which ensure that static analyses accurately gauge runtime behavior, are represented by formulas over such relations. These properties may be fundamental to the language or they may pertain to analyses introduced by individual extensions. We consider the problem of modular metatheory , by which we mean that proofs of relevant properties should be constructible by reasoning independently within each component in the library. To solve this problem, we propose the twin ideas of decomposing proofs around language fragments and of reasoning generically about extensions based on broad, a priori constraints imposed on their behavior. We establish the soundness of these styles of reasoning by showing how complete proofs of the properties can be automatically constructed for any language obtained by composing the independent parts. Precision in these arguments results from framing them within a logic that encodes inductive, rule-based specifications via least fixed-point definitions. We have implemented our ideas in a language specification system called Sterling and a proof assistant called Extensibella and have used them to validate the examples that motivate the theoretical discussions.