Compositional Data Types

A family of Haskell libraries for constructing modular data structures and modular functions.

Source code

Publications:

• Composing and Decomposing Data Types
• Parametric Compositional Data Types
• Compositional Data Types

Modular Tree Automata

A Haskell library for building modular programs on tree structured data, based on (macro) tree transducers.

Source code

Publications:

• Modular Tree Automata
• Programming macro tree transducers

Compilation with Structured Graphs

A prototype demonstrating the use of structured graphs for implementing compilers and reason about their correctness.

Source code

Publication: Proving Correctness of Compilers Using Structured Graphs

Attribute Grammars on Graphs

A library for implementing algorithms on acyclic graphs using attribute grammars.

Source code

Publication: Generalising Tree Traversals to DAGs

Calculating Correct Compilers

A Coq library for building correct-by-construction compilers.

Source code: equational approach; relational approach

Publications:

• Calculating Certified Compilers for Non-Deterministic Languages
• Calculating Correct Compilers

Modular Hoopl

A Haskell library for constructing optimising compilers.

Source code

Certified Financial Contract Management

A certified financial contract management system.

Source code

Publications:

• Certified Symbolic Management of Financial Multi-Party Contracts
• Towards Certified Management of Financial Contracts