Eva: Type Systems for Functional Reactive Programming
Status: Completed
Year: 2021
Supervisor: Prof. Alan Mycroft
Details
This project is my undergraduate dissertation project at Cambridge. It concerns the design, implementation, and evaluation of a practical FRP language called Eva, whose type system is an enhanced version of a recent theoretical calculus called Lively RaTT. Eva’s type system addresses the limitations of modern reactive programming languages by:
- Certifying that all programs possess certain statically-known guarantees
- Ensuring no data resides in the heap for more than one time step during a program’s execution. Programs need to be explicit in their retention of data and, hence, do not exhibit any implicit space leaks.
- Supporting polymorphism and treating all data as first-class citizens, making Eva expressive enough to implement a wide spectrum of programs.
- Providing information on both safety and liveness properties of certain reactive programs via their types, a feature not provided by any other programming language.
As a significant proof of concept, I embedded Lustre, an established dataflow programming language for implementing critical control software, as a domain-specific language within Eva via a program transformation process called Lust4Eva.
Results
You might be interested in the current version of the source code, or the dissertation report itself.