A verified compiler

Compilers take syntax and transform it into code that is executable by a machine, and they do this using various stages: syntax analysis, semantic analysis, code generation, etc. The machine code that is outputted from a compiler is usually trusted by the developer that it is correct, or that it exhibits an equivalent computation to […]

Continue reading

Proving the Correctness of MiniJava Refactorings

The great mathematician and computer scientist, Christopher Strachey, once observed, that, if you can define a programming language’s value domain, you have already said a considerable amount about its semantics. Indeed, if we extend the idea of a value domain, (or a denotational semantics for mapping values in a programming language to their values), to […]

Continue reading

Energy Consumption of Parallel Patterns

For a very long time, the main goal of parallel computing techniques was to improve performance of parallel applications, delivering better speedups without consideration for possibly massively increased power consumption. However, the energy footprint of high-performance servers has become unacceptably high recently, resulting in demand for greener computing and for exploring tradeoffs between application performance […]

Continue reading

Multilevel Parallel Patterns

Parallel patterns represent an important high-level abstraction for programming complex parallel hardware systems and they have been endorsed by several top IT companies that offer their own pattern libraries (e.g. Intel Thread Building Blocks, Microsoft PPL). However, most of these pattern libraries are tailored to shared- memory multicore processors with the “flat” architecture of cores. […]

Continue reading

Using meta heuristics to discover parallelism

After writing a sequential program, often programmers try to parallelise it. However, knowing exactly where in the program to parallelise is often a black art. Sometimes, programmers employ techniques such as profiling to find hotspots in their code and then parallelise those. However, it is well understood that hotspot detection alone is not enough to […]

Continue reading

Using Meta Heuristics to find optimal parallelisations of skeletal programs

Writing parallel programs is a very complex process, as often there exists many different parallelisations of a given problem. Skeleton libraries, such as those for C++, C, Erlang etc, offer generalised abstractions over these parallel behaviours, as higher-order functions. However, many applications can be parallelised using many different skeletons, or, furthermore, can be parallelised using […]

Continue reading

Trustworthy Refactoring in Idris

Refactoring is the process of changing the structure of a program without modifying its behaviour, or functional semantics. Often, refactoring tools are implemented and then the correctness of the transformations is demonstrated correct by vigorous testing or well-formed rewrite rules that the implementation is based on. However, most programming languages do not have a well-formed […]

Continue reading

Parallel Skeletons in Erlang

Parallel Skeletons are generalised higher-order functions for abstracting over the low-level complexities of implementing common parallel algorithmic behaviours. The Skel library (https://skel.weebly.com) is a parallel skeleton library for Erlang, offering a domain specific language (DSL) allowing Erlang programers to write parallel programs quickly and easily.   The focus of this project is to add new […]

Continue reading

Profiling for Energy Hotspots

Non-functional properties, such as time, energy and security, are becoming critically important in areas ranging from small-scale sensors, through smart cyber-physical systems and mobile devices, to data centres, despite it being treated as a secondary concern. As embedded devices become more commonplace, increasing is the pressing demand for more time and energy optimisation in applications […]

Continue reading

Music Generation in Erlang

Computer music generation has become increasingly popular, with devices like the SonicPi and supercollider providing reasonably easy ways to write code that resembles music that is generated. The problem with these systems is that the code one needs to write to produce the music is not useful to real musicians who do not understand code, […]

Continue reading