Computers are good at adding billions of numbers in microseconds. Humans, on the other hand, are good at abstract thinking. This is exemplified by the development of philosophy, literature, science and mathematics.
These observations have deep consequences for programming and the design of programming languages. The overarching concern of our research is to minimize the difference between how humans conceptualise programs and how those programs are implemented in a programming language. To achieve this, we do the same thing humans have been doing for 5000 years as we try to understand the world around us. That is, we construct abstract models --- in this case, abstract models of computation.
For us, there is a symbiotic relationship between mathematics, programming, and the design of programming languages, and any attempt to sever this connection will diminish each component. At the centre of this relationship is the desire to use mathematics to understand the nature of computation, and then to reflect that understanding in programming languages.
The Mathematically Structured Programming group aims to enhance our understanding of the process of computation, and to thereby drive the development of high-level programming languages. Concretely we will use ideas from the following disciplines:
- Functional Programming: What does a high-level programming language look like? Functional programming is currently at the apex of high-level programming languages and so forms our target model of computation.
- Logic: Why is functional programming sucessful as a model of high-level computation? The answer lies in its genesis as a clean implementation of the logical structure of computation. Thus we develop functional programming by studying the logical structure of computation.
- Type Theory: How does one take the logical structure of computation and turn it into a programming abstraction? Type theory allows us to do this by providing a language at an intermediate level of abstraction between a programming language and its logical foundations. Indeed, type theory could be said to be the ideas factory for programming languages.
- Category Theory: How does one understand structure abstractly? One uses category theory - thats how! Ideas such as monads, initial algebra semantics attest to the deep contribution that category theory has made to computation.
Overall, we therefore see the mathematical foundations of computation and high-level programming as inextricably linked. We study one so as to develop the other. The research of the Mathematically Structured Programming group aims to migrate logical, type-theoretic and categorical ideas into functional programming and, reciprocally, to feed challenges back from functional programming into these more mathematical domains. Our aim is to be ahead of the curve in the development of functional programming and studying the mathematical foundations of computation is the way we intend to achieve this.
People, WWW, Email, Photos:
The group was set up on July 1, 2008 at the University of Strathclyde and comprises
- Prof Neil Ghani who is currently working on theories of advanced data types, containers, induction recursion and all areas of category theory. See Neil's current homepage for more details or email Neil.Ghani@cis.strath.ac.uk. And, here is a picture of Neil.
- Dr Patricia Johann who is currently working on advanced data types and categorical and operational models of parametricity. See Patricia's current homepage for more details or email Patricia.Johann@cis.strath.ac.uk. And, here is a picture of Patricia.
- Dr Conor McBride who is currently working on dependently typed programming and, in particular, Epigram. He is also interested in extending the functionality of Haskell so that it can mimic the dependently-typed style of programming. See Conor's current homepage for more details or email Conor.McBride@cis.strath.ac.uk. And, here is a picture of Conor. Perhaps taking abstraction a wee bit too far.
Ever keen to spread the word, Conor is co-organising a workshop on the rather well titled Mathematically Structured Functional Programming. Sounds good to us!
We are always interested in meeting students who share our goals and want to study for a PhD with us. Interested students can contact Prof Ghani at Neil.Ghani@cis.strath.ac.uk
Here are a few of our publications
- d for Data --- Differentiating Data Structures. Neil Ghani, Michael Abbott, Thorsten Altenkirch and Conor McBride. Fundamentae Informatica , vol. 65(1,2), pages 1-28, 2005. [ps.gz]
- Containers - Constructing Strictly Positive Types. Neil Ghani, Michael Abbott and Thorsten Altenkirch. Theoretical Computer Science , vol. 341(1), pages 3-27, 2005. [pdf]
- The Impact of seq on Free Theorems-Based Program Transformations. Patricia Johann and Janis Voigtlaender. Fundamenta Informaticae, Special Issue on Program Transformation, vol. 69 (1,2), pages 63 - 102, 2006. [pdf]
- Selective Strictness and Parametricity in Structural Operational Semantics, Inequationally. Janis Voigtlaender and Patricia Johann. Theoretical Computer Science, vol. 388 (1,3), pages 290 - 318, 2007. [pdf]
- Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08), pages 297 - 308. [pdf]
- The view from the left. Conor McBride and James McKinna. Journal of Functional Programming , vol. 14(1), pages 69-111, 2004. [pdf]
- Applicative programming with effects. Conor McBride and Ross Paterson. Journal of Functional Programming, vol. 18(1), pages 1-13, 2008. [pdf]