Scheme: University Research Fellowship
Organisation: University of Oxford
Dates: Jan 2015-Dec 2019
Summary: I am working on mathematical theories of programming languages. We rely on computer programs every day, but what does a computer program mean? We can see what a simple program does by running it, but that is not so straightforward if the program interacts with people or other programs. So we seek a semantics (meaning) for programming languages.
The theory of computation and programming is of fundamental interest, but it has important applications as it yields techniques for verifying that computer programs are correct, and new ways of specifying programs and notions of program correctness.
I am involved in various approaches to the semantics of programming languages. Recently I have been working on an approach based on a generalization of universal algebra. The idea is to identify notions of computation by specifying when two programs are equal. We can then study these notions of computation by analyzing these algebraic theories. I have used this approach to study various notions of computation including memory allocation, network communication, code with jumps, logic programming, and quantum computing.