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

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

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

Refactorings for Energy Optimisation

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

Refactoring Idris

Refactoring is the process of changing the structure of code without changing its meaning. It has so far been practised every day by developers manually, as they typically rewrite their code to make it more amenable for maintenance, or readability. Since the 1970s, refactoring has also become an automated technique, with many refactoring tools appearing […]

Continue reading

Safety Assurances of Refactorings

A refactoring should transform code such that it maintains functional correctness. In languages such as C++ it can be difficult to the refactoring developer to ensure that their refactoring can be applied safely. This is particularly important when the refactoring transforms the internal behaviour of the program, such as the introduction of parallelism. This project […]

Continue reading