Our vision is to use mathematics to understand the nature of computation, and to turn that understanding into the next generation of programming languages.
We see the mathematical foundations of computation and programming as inextricably linked. We study one so as to develop the other.
This reflects the symbiotic relationship between mathematics, programming, and the design of programming languages — any attempt to sever this connection will diminish each component.
To achieve these research goals we use ideas from the following disciplines:
- Functional Programming
What does the future of programming languages look like? Functional programming languages like Haskell, Agda 2 and Epigram are currently at the apex of programming language design and so form our target model of computation.
Why is functional programming successful as a model of 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—that's how! Ideas such as monads and initial algebra semantics attest to the deep contribution that category theory has made to computation.
MSP101 is an ongoing series of informal talks by visiting academics or members of the MSP group. The talks are usually Thursday 3pm in room LT1310 in Livingstone Tower. They are announced on the msp-interest mailing-list. The list of talks is also available as a RSS feed and as a calendar file. Due to COVID-19, the MSP 101 seminar is now held online. The Zoom link can be found on the msp-interest mailing list and the SPLS Zulipchat.