Correctness of Multistage Notations

The goal is to provide the theoretical foundation for moving away from the classical static compile-link-run model of language semantics to where meta-programming, generative programming, model-driven development, partial evaluation and multistage programming are leading. Here programs are generated from code patterns, from code fragments written in different languages or from components, according to directives expressed through metadata, instantiating a general problem solution to particular cases of the problem. What we need is a practical theory that brings generative programming techniques, which at present are mostly embedded in some tools or language features, under the explicit control of the programmer, providing means to control the structure and the semantical content of generated code.

List of topics to consider:

• More and more code is generated rather than written. By code we mean here first and foremost source code in a higher programming languages, but also GUI descriptions, deployment descriptors, database queries, hyperlinked documentation, web pages, Javascript code embedded in web pages, and so on. The tools and notations used to write the code generators often do not provide even the most elementary guarantees that the generated code is correct.
• Generated code may be checked for correctness on at least four levels: (a) Syntactic well-formedness; (b) Scope well-formedness (when the generated code contains variable binders, cross-references and similar); (c) type correctness (when the generated notation has a static notion of type); and (d) dynamic semantics correctness -- does the generated code mean or do what it is intended to?
• Static correctness guarantees are particularly important for runtime code generation, where a system may fail at runtime due to the faulty generation of code. For code generated at compiletime or build time, a compilation phase will usually check at least correctness (a), (b) and (c) before deployment is attempted, but this is not necessarily the case for code generated at runtime.
• One can even consider runtime "hardware" generation: there are now systems that include FPGA boards, so one can create and configure a specialized co-processor at runtime. Such systems are rather hard to debug, so static guarantees are highly desirable.

Relevant work and people include: Staged computation (Joerring and Scherlis, Lisp/Scheme quasiquotation (backquote and comma), DynJava (Oiwa), MetaML (Sheard), MetaOCaml (Calcagno, Leroy, Taha), Metaphor (Neverov, Roe), dependent types (Martin-Lof, Coquand), the Coq system, Omega (Sheard), Pasalic, Linger, Pfenning, Davies, Nanevski, Pitts, Nielson, Batory, Czarnecki, Smaragdakis, Kamin, explicit substitutions, ...

Challenge: (5 years) Develop a theory of types for multistage languages that covers correctness levels (a), (b), (c) and (d). The theory should support type notations and mechanized consistency checking. Relevant existing theory includes dependent types (Martin-Lof) and nominal logic (Pitts).

Challenge: (5 years) Develop a theory of types to support safe runtime reflection.

Challenge: (5 years) Develop theory to support typesafe database access from a mainstream programming language.