A list of formal and informal projects that I am, or have been, involved in.
- RoboCalc. An EPSRC project exploring development, modelling, and verification techniques for mobile and autonomous robots.
- INTO-CPS. An EU Horizon 2020 project with the goal of producing an integrated tool-chain for model based design of cyber-physical systems.
- 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 was 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.