Relevant Degree Programs
Graduate Student Supervision
Master's Student Supervision (2010 - 2020)
Rust is a new systems programming language designed with a focus on bare metal performance, safe concurrency and memory safety. It features a robust abstraction mechanism in the form of traits, which provide static overloading and dynamic dispatch. In this thesis, we present MiniRust—a formal model of a subset of Rust. The model focuses on the trait system and includes some advanced features of traits such as associated types and trait objects. In particular, we discuss the notion of object safety—the suitability of a particular trait for creating trait objects—and we formally determine very general conditions under which it can be guaranteed. To represent the runtime semantics of MiniRust programs, we develop an explicitly-typed internal language RustIn, for which we prove type safety, and we show that well-typed MiniRust programs can be translated to well-typed RustIn programs. Finally, we adapt the informally-described Rust trait coherence rules to our model and we show thatthey are sufficient to ensure that overloads are always well-determined, even in the presence of library extensions.
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.
Multi-stage programming is a form of metaprogramming that is anextension of ideas and techniques of partial evaluation. This thesisdiscusses a (re)implementation of a multi-stage programming systemMetaOCaml. The system presented here differs from the OCamlimplementation by Taha et al in that it is implemented on top of amodern OCaml compiler. It differs from BER MetaOCaml in that itsupports generation of native code in a turn-key fashion. It differsfrom both systems in that it uses the OCaml intermediate representationto represent the notion of code (to the best of my knowledge, existingsystem use abstract syntax trees instead.)