The use of formal methods for ensuring software quality is undergoing a renaissance, with many exciting new developments in verification, correctness and proof. Simon Peyton-Jones, FRS and Microsoft Senior Researcher, describes types as “the world’s most successful formal method.”

At DSG, we are working on a range of proof-theoretic methods that can enhance programming language reliability and usability.

Examples of projects include:

1. EPSRC grant Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a
   new generation of programming languages, 2013-2017. Joint with John Power, University of Bath.

2. SICSA Industrial “Proof of Concept” grant
   Machine-Learning for Industrial Theorem Proving, 2013-2014. Joint with Jonathan Heras.

3. EPSRC First Grant scheme; project title
   Machine-Learning
   Coalgebraic Automated Proofs, 2012-2014.

   Associated with this grant is the project on ML4PG, on data mining proofs in Coq via Proof General interface.