Computer & Information SciencesMathematically structured programming
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.
Our research covers many topics in the mathematical foundations of Computer Science, including Denotational Semantics, (Applied) Category Theory, Type Theory and Logic.
Our Research
To achieve our research goals we use ideas from the following disciplines:
Functional Programming and Type Theory
What does the future of programming languages look like? 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.
In this area, Dr. Robert Atkey is PI on the EPSRC funded project AISEC: AI Secure and Explainable by Construction, jointly with Heriot-Watt University and the University of Edinburgh. The MSP part of this project is applying type theory to the construction and verification of AI powered systems.
Prof. Neil Ghani and Drs. Conor McBride and Fredrik Nordvall Forsberg are engaged in the NPL funded Trusted Systems project that seeks to apply Type Theory and Functional Programming to trustworthy scientific programming.
Logic
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. We also study logical and algebraic techniques in their own right, using modal logics and quantitative algebras to study dynamic and approximate properties of systems.
In the field of Coalgebraic Modal Logic, Dr. Clemens Kupke is PI on the Leverhulme funded project COVER: Coalgebraic Foundations for Quantitative Verification, jointly with the University of Southampton.
Prof. Radu Mardare is an originator of the theory of Quantitative Algebraic Theories, used to give a rigorous foundation for approximate comparison of systems’ behaviour.
Category Theory
How does one understand structure abstractly? How can one build theories that systematically build complex systems by composing descriptions of simpler ones? 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.
Dr. Jules Hedges is applying Category Theory to build a compositional theory of Strategic Game Theory via the theory of Open Games. The compositionality of this theory allows complex game-like situations to be built from simple parts. Open Games are being used to construct models of involved economic situations.
We have a lively community of 9 members of faculty staff, 3 postdoctoral researchers and 18 PhD students. Please see our working webpages at https://msp.cis.strath.ac.uk/ for more information. We are actively seeking new PhD students to be part of our group. Please contact any of our researchers whose work interests you, or contact the group leader Robert Atkey (robert.atkey@strath.ac.uk).
MSP 101
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.
