Calculating Correct Compilers

Graham Hutton

(University of Nottingham)

In this talk we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high-level semantics by systematic calculation, with all the required compilation machinery falling naturally out of the calculation process. The approach is based upon the use of standard equational reasoning techniques, and has been applied to calculate compilers for a wide range of language features and their combination. The talk will explain the basic ideas using a small example language, and is aimed at a general audience.

Speaker Bio: Graham Hutton is Professor of Computer Science at the University of Nottingham, where he co-leads the Functional Programming Lab. He is an editor of the Journal of Functional Programming, member of IFIP WG 2.1 on Algorithmic Languages and Calculi, and has served as Vice-Chair of the ACM Special Interest Group on Programming Languages and Steering Committee Chair of the International Conference on Functional Programming. His research interests are in developing simple but powerful techniques for writing and reasoning about programs, by recognising and exploiting their underlying mathematical structure. His book Programming in Haskell was published by Cambridge University Press in 2007.

Thursday 22nd January 2015, 15:00
Board Room
Department of Computer Science