Graham Hutton
Professor of Computer Science at the University of Nottingham
Co-leader of the Functional Programming Lab
My research interests are in the mathematics of program construction. The aim of my research is to develop simple but powerful techniques for writing and reasoning about computer programs, by recognising and exploiting their underlying mathematical structure. Most of my work takes place in the context of functional languages such as Haskell and Agda.
I'm director of the Midlands Graduate School, board member of the Haskell Foundation, an editor of the Journal of Functional Programming, and an ACM Distinguished Scientist. I've also served as vice-chair of the ACM Special Interest Group on Programming Languages and steering committee chair of the International Conference on Functional Programming.
Simplicity is a great virtue but it requires hard work to achieve it and education to appreciate it. And to make matters worse: complexity sells better.
-- Edsger Dijkstra
Activities
Current and recent activities:
- Director, Midlands Graduate School, 2023-date
- Board member, Haskell Foundation, 2022-date
- Editor, Journal of Functional Programming, 2014-date
- Co-editor, JFP Special Issue on Program Calculation, 2023-2024.
- Principal investigator, Semantics-Directed Compiler Construction, 2024-2027
- Program co-chair, Functional Software Architecture - FP in the Large, Seattle, 2023.
- Program committee, Haskell Symposium, Seattle, 2023
- Award committee, ACM SIGPLAN Distinguished Eductator Award, 2021-2024
- Advisory board, EPSRC Network on Model Driven Engineering, 2022-date
- Steering committee, Functional Software Architecture - FP in the Large, 2024-date.
- Steering committee, Mathematics of Program Construction, 2017-date.
- Member, IFIP Working Group 2.1 on Algorithmic Languages and Calculi, 2004-date
- Member, EPSRC Peer Review College, 2006-date
Publications
A list of publications, bibtex entries, and citations, is available, or you can select below:
- Quotient polymorphism (2024)
- Calculating compilers effectively (HASKELL 2024)
- Beyond trees: calculating graph-based compilers (ICFP 2024)
- HoTT operads (2024)
- Quotient Haskell: lightweight quotient types for all (POPL 2024)
- Programming language semantics: it's easy as 1,2,3 (JFP 2023)
- Calculating compilers for concurrency (ICFP 2023)
- Subtyping without reduction (MPC 2022)
- Monadic compiler calculation (ICFP 2022)
- Calculating dependently-typed compilers (ICFP 2021)
- Calculating correct compilers II: return of the register machines (JFP 2020)
- Pre-ordered metric spaces for program improvement (2020)
- Liquidate your assets: reasoning about resource usage in Liquid Haskell (POPL 2020)
- Proceedings of the MPC conference (MPC 2019);
- Call-by-need is clairvoyant call-by-value (ICFP 2019)
- Theorem proving for all: equational reasoning in Liquid Haskell (HASKELL 2018)
- AutoBench: comparing the time performance of Haskell programs (HASKELL 2018)
- Parametric polymorphism and operational improvement (ICFP 2018)
- Improving Haskell (TFP 2018)
- Compiling a 50-year journey (JFP 2017)
- Failing faster: overlapping patterns for property-based testing (PADL 2017)
- Programming in Haskell (CUP 2016)
- Contractive functions on infinite data structures (IFL 2016)
- Cutting out continuations (WF 2016)
- Calculating correct compilers (JFP 2015)
- Programs for cheap! (LICS 2015)
- Towards a theory of reach (TFP 2015)
- Worker/wrapper/makes it/faster (ICFP 2014)
- Work it, wrap it, fix it, fold it (JFP 2014)
- The under-performing unfold (IFL 2013)
- Compilation à la carte (IFL 2013)
- Representing contractive functions on streams (2011)
- Towards modular compilers for effects (TFP 2011)
- Factorising folds for faster functions (JFP 2010)
- Compiling concurrency correctly: cutting out the middle man (TFP 2009)
- The worker/wrapper transformation (JFP 2009)
- Modularity and implementation of mathematical operational semantics (MSFP 2008)
- Towards a verified implementation of software transactional memory (TFP 2008)
- Reasoning about effects: seeing the wood through the trees (TFP 2008)
- What is the meaning of these constant interruptions? (JFP 2007)
- Programming in Haskell (CUP 2007)
- Compact fusion (MSFP 2006)
- Accurate step counting (IFL 2005)
- Report on the BCTCS colloquium (BCTCS 2005)
- Proof methods for corecursive programs (FI 2005)
- Calculating an exceptional machine (TFP 2004)
- Compiling exceptions correctly (MPC 2004)
- Proceedings of the APPSEM workshop (APPSEM 2003)
- The countdown problem (JFP 2002)
- Special double issue on Haskell (JFP 2002)
- The generic approximation lemma (IPL 2001)
- When is a function a fold or an unfold? (CMCS 2001)
- Proceedings of the Haskell workshop (HASKELL 2000)
- Proof methods for structured corecursive programs (SFPW 1999)
- A tutorial on the universality and expressiveness of fold (JFP 1999)
- Fold and unfold for program semantics (ICFP 1998)
- Monadic parsing in Haskell (JFP 1998)
- Monadic parser combinators (1996)
- Back to basics: deriving representation changers functionally (JFP 1996)
- Bananas in space: extending fold and unfold to exponential types (FPCA 1995)
- Categories, allegories, and circuit design (LICS 1994)
- The Ruby interpreter (1993)
- A relational derivation of a functional program (STOP 1992)
- Between functions and relations in calculating programs (1992)
- Higher-order functions for parsing (JFP 1992)
- A calculational theory of pers as types (1992)
- Making functionality more general (GWFP 1992)
- Functional programming with relations (GWFP 1991)
- Parsing using combinators (GWFP 1990)
Videos
YouTube channel: Teaching videos: Computerphile videos:- Program correctness
- Tail recursion
- Curried functions
- Functional parsing
- To infinity and beyond
- What is a monad?
- The Y combinator
- Lambda calculus
- A secret of sorting
- Podcast (Haskell Foundation)
- Calculating correct compilers (Haskell eXchange)
- Programming in Haskell (FutureLearn)
- How to be more productive (Channel 9)
- Calculating an exceptional machine
- The countdown problem (Channel 9)
Teaching
Current teaching:
- Functional programming (1st year course)
- Advanced functional
programming (2nd year course)
Previous teaching:
- Introduction
to category theory (postgraduate course)
- Introduction to domain theory (postgraduate course)
- Principles of
programming languages (3rd year course)
- Concepts of
concurrency (2nd year course)
People
Research fellows:
- Brandon Hewer, Semantics-Directed Compiler Construction, 2024-2027
- Jennifer Hackett, Unified Reasoning About Program Correctness and Efficiency, 2016-2021
- Nils Anders Danielsson, Reasoning About Exceptions and Interrupts, 2007-2010
- Joel Wright, Compiler Correctness, 2005
Current PhD students:
- Sky Wilshaw, Semantics of Memory Safety and Borrowing
- Zac Garby, Compiler Calculation for Effectful Languages
- Mitchell Pickard, Dependent Types for Compiler Calculation
Former PhD students:
- Brandon Hewer, Types With Extra Structure: Predicates, Equations, Composition, 2024
- Martin Handley, Efficiency Three Ways: Tested, Verified, and Formalised, 2020
- Jonathan Fowler, Narrowing in on Property-Based Testing, 2019
- Jennifer Hackett, The Worker/Wrapper Transformation, 2017
- Ambrus Kaposi, Type Theory in a Type Theory with Quotient Inductive Types, 2016
- Laurence Day, The Modular Compilation of Effects, 2015
- Liyang Hu, Compiling Concurrency Correctly, 2012
- Mauro Jaskelioff, Lifting of Operations in Modular Monadic Semantics, 2009
- Catherine Hope, A Functional Semantics for Space and Time, 2008
- Joel Wright, Compiling and Reasoning about Exceptions and Interrupts, 2005
- Paul Blampied, Structured Recursion for Non-Uniform Data-Types, 2000
- Anthony Daniels, A Semantics of Functions and Behaviours, 1999
- Colin Taylor, Formalising and Reasoning about Fudgets, 1998
Projects
The 'mind the gap' project was featured in impact magazine.
- Semantics-Directed Compiler Construction: From Formal Semantics to Certified Compilers
Principal investigator, EPSRC, £912,000, 2024-2027 - Mind the Gap:
Unified Reasoning About Program Correctness and Efficiency
Principal investigator, EPSRC, £424,000, 2016-2021 - Reasoning About
Exceptions and Interrupts
Principal investigator, EPSRC, £306,000, 2007-2010 - Midlands Graduate School in the Foundations of
Computing Science
Principal investigator, EPSRC, £39,000, 2007-2009 - British Colloquium for Theoretical
Computer Science
Co-investigator, EPSRC, £65,000, 2008-2010 - British Colloquium for Theoretical
Computer Science
Co-investigator, EPSRC, £24,000, 2005-2007 - IST Working Group on Applied Semantics II
Site leader, £250,000, 2003-2006 - Concurrent Haskell
Principal investigator, Microsoft Research, £25,000, 2001-2004 - ESPRIT Working Group on Applied Semantics
Site leader, £190,000, 1998-2002 - Structured Recursive Programming
Principal investigator, EPSRC, £11,000, 1997-2000
Personal
I'm from Glasgow in Scotland. After completing a PhD at the University
of Glasgow, I spent a few years as a researcher in Gothenburg and
Utrecht, before moving to Nottingham where I am Professor of
Computer Science. I'm married to the lovely Annette, and we have
two grown up sons. In my spare time I enjoy cars, cooking,
board games, and restoring our house.
Contact
| Twitter: | @haskellhutt |
| YouTube: | @haskellhutt |
| Email: | graham.hutton@nottingham.ac.uk |
| Phone: | I don't have an office phone and my university number is inactive |
| Address: | Professor Graham Hutton School of Computer Science University of Nottingham Jubilee Campus, Wollaton Road Nottingham NG8 1BB United Kingdom |