Refining semantics for multi-stage programming

Multi-stage programming is a programming paradigm that supports runtime code generation and execution. Though researchers have extended several mainstream programming languages to support it, multi-stage programming has not been widely recognised or used. The popularisation of multi-stage programming has been impeded by the lack of development aids such as code refactoring and optimisation, for which the culprit is the lack of static analysis support. Van Horn and Might proposed a general-purpose approach to systematically developing static analyses for a programming language by applying transformations to its formal semantics, an approach we believe is applicable to multi-stage programming. The approach requires that the initial semantics be specified as an environmental abstract machine that records the change of control strings, environments and continuations as a program evaluates. Developing an environmental abstract machine for a multi-stage language is not straightforward and has not been done so far in the literature. In the thesis, we study multi-stage programming through a functional language, MetaML. The main research problem of the thesis is: Can we refine the pre-existing substitutional natural semantics of MetaML to a corresponding environmental abstract machine and demonstrate their equivalence? We first develop a substitutional structural operational semantics for MetaML. Then we simplify the research problem along two dimensions—each dimension leads to a less complicated semantics refinement problem. The first dimension is to refine semantics for a single-stage language rather than a multi-stage language: we stepwise develop an environmental abstract machine, the CEK machine, for a single-stage language, ISWIM, based on its substitutional structural operational semantics. The second dimension is to derive a substitutional abstract machine rather than an environmental abstract machine: we stepwise develop a substitutional abstract machine, the MK machine, for the multi-stage language MetaML, based on its substitutional structural operational semantics. Finally, utilising the experience of refining semantics along two dimensions, we stepwise develop an environmental abstract machine, the MEK machine, for MetaML, based on its substitutional structural operational semantics. Furthermore, we introduce three proof techniques which are used throughout the thesis to prove the equivalence of semantics.Science, Faculty ofComputer Science, Department ofGraduat