A list of formal and informal projects that I am, or have been, involved in.
- Isabelle/UTP. A proof environment for Hoare and He's Unifying Theories of Programming in Isabelle/HOL.
- Regular Algebras. An implementation of the algebraic hierarchy in Isabelle/HOL.
- Symphony. An Eclipse-based development environment for CML. I am responsible for the theorem prover plugin.
- COMPASS. EU FP7 Project on Formal Modelling and Analysis of "Systems of Systems".
- Agda. A dependently typed programming language and proof assistant.
- Higher-order Refinement Techniques for Model Driven Architecture. EPSRC project on MDA.
- Cashew. Process algebraic formal semantics for semantic web services.
- Haskell Interoperation Framework. A partial implementation of the Web service stack in Haskell.