Active Projects

• Using Agda to verify properties of the non-optimising compiler for the Reduceron.
• Optimus Prime - An implementation of supercompilation for the f-lite language, particularly targeting the Reduceron.
• Playing with theorem provers to verify properties of compilers.

Previous Work

• Implementing semantics for a toy imperative language in the Alloy relational logic.