• 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 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
      Coalgebraic Automated Proofs
      , 2012-2014.

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