Making our digital devices trustworthy and efficient
Our modern life depends on digital devices, from mobile phones to digital banking to weather forecasting. These devices rely on a technology known as multi-core to make them run in a way that is both efficient and low in energy usage (this is particularly important for software running on devices powered by a battery). Multi-core software is, however, extremely difficult to write, expensive to produce, and potentially very error prone as a result. In this project we are utilising a special kind of programming language known as a dependently typed language. A dependently typed programming language enables developers to write applications that have special kinds of guarantees which must be adhered to when the device is running. In this project we show how we can use these dependently typed programming languages to build safe and efficient multi-core software for our modern digital world.
Keywords
Programming Languages, Parallelism, Multi-Core, Dependent Types