Modular metatheory for extensible languages

Abstract

The features available in a programming language affect how easy it is to write programs for different purposes using it. Extensible languages allow specifications of language features to be developed independently of one another, then composed to form a new language containing all the features from all the specifications included. This lets programmers choose language features they find useful for each program they write. However, because the specifications of different language features are developed independently of one another, we do not know the language resulting from composition is well-formed in desired ways. In particular, we don’t know what properties should be true of the language, nor do we have a proof that they are true; that is, we do not have metatheory, a set of properties proven to be true, for the language. Metatheoretic properties are known to hold for any program written in the language, providing useful information to programmers about what can and cannot happen in a program. For example, the type preservation property can be stated as terms with a certain type evaluate to values of the same type, and guarantees well-typed programs cannot encounter type errors during evaluation. In an extensible setting, proving properties will hold for any composed language is difficult because the full language is not created until the time of composition. This thesis develops a modular approach to establishing the metatheory of extensible languages written using a framework where modules specifying language features may build on others. In this approach, each specification module independently introduces new metatheoretic properties expected to hold for any composed language that includes the module. The work of proving these properties for any composed language is distributed across modules, with each module contributing proofs for the new properties it introduces and those of the modules on which it builds. These proofs are written in the limited context of a single module’s knowledge but need to reason about the larger contexts of composed languages, which may include constructs unknown to the module writing the proof. To address this, we utilize generic reasoning to handle the currently-unknown additions that may be present in a composed language. When a language composition is built, the proofs from each module are then used to create a composed proof for each property. These composed proofs guarantee each property from each module included in the composition holds for the composed language, bringing the benefits of metatheory to the extensible setting. In addition to developing a reasoning framework for modular metatheory, we implement it in an interactive proof assistant named Extensibella. Extensibella aids users in writing modular proofs. It does this by adding an extra layer to Abella, an existing proof assistant. This extra layer checks the proofs are valid in the context of a single module and that generic reasoning is carried out correctly, then passes proofs to Abella to check their validity in the logic G in which it constructs proofs. Extensibella also includes functionality to compose the proofs from individual modules to form full proofs of properties for any composed language. To support this implementation, we have also implemented the framework for language specification about which we reason in a system named Sterling. Sterling allows users to write language specifications and check them for their modular validity, then produces specifications Extensibella can read and about which it can reason. Finally, using these implementations, we have developed a set of example extensible languages and their metatheory. These applications suggest our framework’s structure does not induce significant limits on what we can prove, so modules can introduce interesting new syntax, semantics, and metatheoretic properties. They also allow us to examine the trade offs in our framework between the freedom given to modules to introduce interesting new syntax and semantics and the ability to introduce and prove new metatheoretic properties.