Theorem Proving for Programming Languages
The use of formal methods for ensuring software quality is undergoing a renaissance, with many exciting new developments in verification, correctness and proof. Simon PeytonJones, FRS and Microsoft Senior Researcher, describes types as “the world’s most successful formal method.”
At DSG, we are working on a range of prooftheoretic methods that can enhance programming language reliability and usability.
Examples of projects include:

EPSRC grant Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a
new generation of programming languages, 20132017. Joint with John Power, University of Bath. 
SICSA Industrial “Proof of Concept” grant
MachineLearning for Industrial Theorem Proving, 20132014. Joint with Jonathan Heras. 
EPSRC First Grant scheme; project title
MachineLearning
Coalgebraic Automated Proofs, 20122014.Associated with this grant is the project on ML4PG, on data mining proofs in Coq via Proof General interface.