An abstract state machine for functional reactive programming
Reactive programming is a paradigm that focuses on data flows and propagation of change. Spreadsheet programming is a form of reactive programming, and more recently reactive languages like Elm have been gaining traction. Unlike their non-reactive (imperative, object-oriented, functional) cousins, there is little or no existing work on specifying the core operational semantics of reactive languages using abstract state machines.
An interpreter for a programming language can be implemented as a state machine. A state represents the entire state of the interpreter (current instruction, heap, stack). The machine defines a transition function that computes successor states for a given input state. Like an ordinary interpreter, successor states for example depend on the type of instruction of the input state. Starting from an initial program evaluation state, interpretation then consists of exploring all possible successor states, which results in a state graph for that program. Interpretation ends when there are no new (previously unencountered) states to be explored.
Abstract state machines hit a sweet spot in expressing programming language semantics: the resulting state-graph is low-level enough to reason over program properties, yet state machines are easy to implement because they are close to “actual” interpreters (closer than for example purely mathematical calculi). Exposing the small steps an interpreter for a reactive language has to take to evaluate reactive programs, and cutting away all non-essential complexity in the process, opens up avenues of further research into reactive language design, implementation, and analysis.
The goal of the thesis is to design and implement an abstract state machine that represents the core concrete semantics of functional reactive programming. The input language for the machine should be expressive enough to support the functional reactive paradigm, but nothing more. In a second step, this abstract machine is further abstracted to represent some finite abstract semantics, which can be used to perform static analysis.
We propose to look at Elm as a concrete example of a reactive language, and the thesis should demonstrate that it is indeed possible to map (simple) Elm programs or programming constructs onto the machine’s input language. Likewise, the transition function should faithfully reflect reactive semantics, and again we propose to look at Elm as a driver for this. You are free to choose the implementation language, but Racket, Scala, or Haskell are highly recommended.
These are the proposed steps for completing this master thesis.
- Based on the research training, choose the functional reactive programming constructs that you want to support.
- Co-design the state-space and the input language of the abstract machine.
- Demonstrate by example that the machine provides the desired concrete semantics.
- Demonstrate applicability by mapping (simple) real-world functional reactive programs onto the input language of the machine.
- Demonstrate usefulness by abstracting the abstract machine to perform some program analysis through examining resulting state-graphs.
This master thesis covers a broad range of topics, is theoretical in nature, and requires strong programming skills.
Research Training
In this part of the thesis, you will read up on all the topics related to the actual design and implementation of the abstract machine for functional reactive languages. Results of the work you do during research training should go into (at least) the ‘Introduction’ and ‘Related Work’ chapters of your thesis. These are the proposed action points.
- Perform literature study on use of abstract state machines (CEK, CESK, ...) as a means for expressing program semantics. Examine abstract state machines for lambda calculus and simple Scheme programs.
- Read up on abstract interpretation of state machines as a foundation for static analysis.
- Study the functional reactive paradigm, and more specifically Elm.
- Explore related work on operational semantics for reactive languages, preferably using abstract machines and for Elm.
CE(S)K machines
- http://matt.might.net/articles/cek-machines/
- http://matt.might.net/articles/cesk-machines/
- http://www.cl.cam.ac.uk/~mom22/fp/lec3-opsem2.pdf
- http://www.cs.indiana.edu/l/www/pub/techreports/TR218.pdf
Abstract interpretation
- http://matt.might.net/papers/vanhorn2010abstract.pdf
- http://en.wikipedia.org/wiki/Abstract_interpretation
- http://santos.cis.ksu.edu/schmidt/Escuela03/WSSA/talk1p.pdf