Compositional Data Types
A family of Haskell libraries for constructing modular data structures and modular functions.
Modular Tree Automata
A Haskell library for building modular programs on tree structured data, based on (macro) tree transducers.
Compilation with Structured Graphs
A prototype demonstrating the use of structured graphs for implementing compilers and reason about their correctness.
Attribute Grammars on Graphs
A library for implementing algorithms on acyclic graphs using attribute grammars.
Publication: Generalising Tree Traversals to DAGs
Calculating Correct Compilers
A Coq library for building correct-by-construction compilers.
A Haskell library for constructing optimising compilers.
Certified Financial Contract Management
A certified financial contract management system.