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