Projects

A list of formal and informal projects that I am, or have been, involved in.

• CyPhyAssure. My EPSRC fellowship project on Compositional Safety Assurance for Cyber-Physical Systems.
• Isabelle/UTP. A proof environment for Hoare and He’s Unifying Theories of Programming in Isabelle/HOL.
• 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.
• 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.