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

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

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