WG211/M23VanWyk

There is a longstanding interest in our community in language extension and mechanisms for easily adding (domain-specific) features to programming languages. One notion of extensibility argues that language extensions should be independently developed such that a programmer can pick the ones needed for their task at hand and compose them with a host language. Previously we have developed some ways to ensure that the composition of language and extension specifications leads to deterministic parsers and well-defined attribute grammars to implement the language.

Recently, Dawn Michaelson, Gopalan Nadathur, and I have been working to establish a modular approach to reasoning about metatheoretic properties for extensible languages. One aim is to ensure that properties established by a host language continue to hold when language extensions are added to the mix. For example, how can a type preservation property introduced by the host language be guaranteed to hold when new extensions that engage in type checking of their new constructs are added? Another aim is to also allow language extensions to introduce new properties that still hold when other extensions, unaware of the property, are added in. An extension that allows variables to be marked as secret or public may wish to establish a property that secret data never leaks to public variables; how is this property established in the presence of other extensions? This talk will discuss some initial techniques and tools we have developed to address these challenges.