Details of Grant 

EPSRC Reference:	EP/Y010744/1
Title:	Semantics-Directed Compiler Construction: From Formal Semantics to Certified Compilers
Principal Investigator:	Hutton, Professor G
Other Investigators:
Researcher Co-Investigators:
Project Partners:	Huawei Group INRIA IT University of Copenhagen Meta (Previously Facebook) University of Cambridge University of St Andrews
Department:	School of Computer Science
Organisation:	University of Nottingham
Scheme:	Standard Research
Starts:	01 April 2024	Ends:	31 March 2027	Value (£):	466,425
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:	EP/Y010035/1
Panel History:	Panel Date Panel Name Outcome 03 Jul 2023 EPSRC ICT Prioritisation Panel July 2023 Announced
Summary on Grant Application Form
Compilers are central to computing, translating programs written by people into code for machines. Some aspects of compiler development, such as syntax analysis, bridge the theory and the implementation in a principled way, with lexers and parsers being algorithmically derived from high-level specifications. On the other hand, there is currently an unbridged gap between the theoretical specification of a programming language, given by a formal semantics, and the code produced by the compiler. Relating the two post hoc is possible, but difficult and rarely done. However, it doesn't have to be this way. A more principled approach is to begin with a semantics for the language, and seek to derive an implementation that is correct-by-construction. The investigators (Graham Hutton and Dan Ghica) have independently developed two such methodologies, which are based on complementary approaches to semantics (evaluators and abstract machines), but utilise different approaches to syntax (trees and graphs). The aim of this project is to reconcile the two methodologies to develop scalable and reusable frameworks for constructing certified compilers from semantics. The project combines the strengths of two leading research groups, is enhanced by a team of expert collaborators (Patrick Bahr, Mario Lavarez-Picallo, Edwin Brady, Simon Marlow, Anil Madhavapeddy, and Beniamino Accattoli), and is supported by fully-funded PhD studentships from the host departments.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.nottingham.ac.uk