51cg

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. Please see our for more information.

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.

Logic

Different logics are suitable for expressing and verifying different properties of programming languages or systems. We make use of a range of methods such as proof theory and coalgebra to understand the computational nature of proofs and systems intended to run without interruption. Those methods are driven by emerging problems in areas such as AI and security. We have particular strengths in modal logic, quantitative properties of systems, and logics for reasoning about concurrency."

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.

Please see our 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, Fredrik Nordvall Forsberg (fredrik.nordvall-forsberg@strath.ac.uk).

MSP 101 Seminar

MSP101 is an ongoing series of informal talks by visiting academics or members of the MSP group. See for information about upcoming and past talks.