This researches mathematically sound yet convenient techniques for manipulating and reasoning with programs, with particular strengths in the functional and relational paradigms and in generic programming. It seeks patterns in specifications, algorithms and programs, and abstracts these patterns to derive solutions to general classes of problems. An active weekly seminar forms a national hub in the mathematics of program construction, with regular participation by colleagues from other universities. Achievements include Hinze's ground-breaking work on generic programming, the basis of Generic Haskell and Generic Clean, Spivey's patent on Profiling Computer Programs, the first treatment of Functional Quantum Computing by Mu and Bird at APLAS'01, and the first rigorous presentation of Arithmetic Coding by Bird, Gibbons and Stratford at AFP'03. Gibbons secured EPSRC funding for Datatype-Generic Programming and Generic and Indexed Programming. Bruno Oliveira won the best paper award at TFP'06 for Extensible and Modular Generics for the Masses.
