Student projects 2019


A Reactive Scratch compiler

MPhil project

Context

Reactive Scratch is a programming language and IDE aimed at teaching programming to children. Reactive Scratch aims to improve Scratch, currently the most widely used platform to teach programming to schoolchildren.

Scratch is based on a very simple imperative language with structured control flow, in the style of IMP. Such a programming language is woefully inadequate for reactive programming, that is, programming where the main action of the program is to react to outside events that it does not control - which is typical of what children want to write: small video games or interactive animations. Reactive Scratch is instead based on Esterel, a reactive programming language based around the primitives of concurrency, signals, and preemption, and which was designed for reactive programming.

Currently, Reactive Scratch exists as a prototype: (1) The IDE is a fork of the Scratch IDE. The language runtime is a naive Esterel interpreter written in BuckleScript (a variant of OCaml), following the constructive operational semantics of Potop-Butucaru et al. This works fine to demonstrate the concept to other computer scientists, but is far too slow to be usable by schoolchildren. (2) Reactive Scratch does not have feature parity with Scratch: it is missing primitives to control dynamic creation and interaction of threads.

There are well-known methods to compile Esterel efficiently to circuits for embedded systems. However, (1) efficient compilation to hardware is based on concurrently executing all the parts of the program, which is expensive and undesirable for execution in a web browser, and (2) Reactive Scratch needs to extend Esterel with primitives that violate the usual assumptions about Esterel compilation.

Project

The project would involve (1) designing and writing a compiler from Reactive Scratch to efficient Wasm (or a really fast interpreter), and (2) designing and implementing primitives to make Reactive Scratch have feature parity with Scratch. The constraints of the latter are likely to strongly influence the successful design of the former. (3) Testing on actual human beings (ideally, schoolchildren, but that might be too much of an effort to organise) whether they find Reactive Scratch helpful, using qualitative methods like semi-structured interviews.

The research outcomes would be (1) the development of a new compilation method from Esterel to be executed in a web browser, and (2) of a new compilation method to support the new primitives of Reactive Scratch, and (3) if time allows, a qualitative assessment of whether people find reactive programming easier in a reactive programming language.

Requirements

The student should have a good grasp of the following topics:

Project supervisors

Jean Pichon-Pharabod and Neel Krishnaswami

(email jp622 to talk to if interested)

References


Mechanising an abstract model checker

MPhil project

Context

Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Model checking faces a "state explosion" problem: the number of states in a realistic system is often too large to be explored exhaustively, if not infinite. One way to tackle this is abstraction: instead of checking the actual model, it is sometimes sufficient to check a simplified model. If the abstract model simulates the concrete model, then any universal property satisfied by the abstract model is satisfied by the concrete model. However, this is rather limiting. Abstract interpretation makes it possible to go beyond this: if there is a Galois connection relating the complete lattice of sets of states of the concrete model and a complete "abstract" lattice, then any property satisfied by the abstract model induced by the Galois connection (for an enriched notion of model and of satisfaction) is satisfied by the concrete model.

Project

The project would involve (1) specifying the notion of satisfaction of a CTL* proposition by a model in the Agda proof assistant; implementing a naive CTL* model checker; and then verifying correctness of the model checker. (2) Implementing an "abstract" model checker that exploits abstract interpretation, and relating it to plain model checking.

Possible extensions of the project could involve implementing various abstract domains, or optimising the performance and memory use of the model checkers.

The research outcomes would be (1) providing some automation to Agda users through reflection, and (2) making this incredibly neat yet unfortunately rather niche meeting of two research communities meet a third research tradition.

Requirements

The student should have a good grasp of the following topics:

Project supervisors

Jean Pichon-Pharabod and Neel Krishnaswami

(email jp622 to talk to if interested)

References

Last modified: 8 Oct 2019