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:
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.
Associated with this grant is the project on ML4PG, on data mining proofs in Coq via Proof General interface.