Ensuring Non-interference of Composable Language Extensions
Channel: Splash Conference 2017
Date: 2017-11-05

Ted Kaminski, Eric Van Wyk
Extensible languages and extensible compiler frameworks aim to allow independently-developed language extensions to be used by a programmer that need not be an expert in language or compiler design. It should be easy to combine the extensions and the resulting compiler should “just work” as expected. Previous work shown how specifications for parsers (based on context free grammars) and for semantic analysis (based on attribute grammars) can be automatically and reliably composed, ensuring that the resulting compiler does not terminate abnormally.

However, this work does not ensure that a property proven to hold for a language (perhaps an extended language) still holds when another extension is added to it, a problem we call “interference.” This paper presents a solution to the problem of interference between language extensions, through the use of a logical notion of “coherence.” We show that a useful class of language extensions, implemented as attribute grammars, preserve all coherent properties. If we also restrict extensions to only making use of coherent properties in establishing their correctness, then the correctness properties of each extension will hold even when composed with unknown other extensions. As a result, there can be no interference: each extension behaves as specified.