Mechanized Operational Semantics


EPSRC Standard Research Grant GR/M98555/01, GPB 151,724


July 2000 - September 2003


The aim of the project is to investigate the viability of using a theorem prover for reasoning about programming language properties in general, and compiler optimisations in particular. The project will be a large scale development of both the theory and practice of computer aided (or mechanised) reasoning and will deliver an end product of a monadic calculus for analysing compiler optimisations, together with a library of tools for syntax representation and tactical verification for: a) the specification of program syntax and semantics of a (functional) higher order imperative language, ML-small, at varying levels of abstraction and detail: b) formal verification of the relative correctness of such semantics: c) proofs of language properties, such as type soundness: and d) proofs of equivalences of program code, and correctness of compiler optimisations. While the entire programme will be of general interest to language designers and compiler writers, it is the compiler optimisation proofs which may have the most direct payoffs. We will be providing a framework in which the details of such optimisations can be studied effectively, potentially producing results which could have an impact on real compilers.


R Crole (Principal Investigator) and Simon Ambler

Other Information:

This project resulted in the founding of the MERLIN workshops, 2001 (at IJCAR), 2003 (at PPDP), 2005 (at ICFP). RC is on the steering committee, and the 2005 PC.

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc
E: MSc

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom


DisabledGo logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.