The Research Interests of the Programming Languages and Systems research group are listed by the interests of individual members.
Mark Batty develops rigorous mathematical specifications, testing tools, and verification techniques for real-world concurrent systems, focusing on established interfaces (e.g. C, C++ and, OpenCL) and concrete testable artefacts (e.g. x86, Power, ARM CPUs, and Nvidia, AMD GPUs). His interests span a variety of complementary topics including: empirical testing of the behaviour of hardware and compilers, building formal models of parts of the system, the development of algorithms and data-structures that use fine-grained concurrency, and the verification of those pieces of concurrent code.
Laura Bocchi’s research spans several areas, which include software engineering, concurrency and formal methods. She is interested in theories and tools for developing safe distributed systems. She is particularly interested in the formal foundations of service coordination and composition, business processes and their transactional behaviour, and the theory and application of behavioural types. Most recently, Laura has been working on the extension of Multiparty Session Types with logics to enable Design by Contract for concurrency, and the effective verification of real-timesystems.
David Castro-Perez is interested in a range of topics, such as programming language semantics, type theory, domain-specific languages, high-level recursion patterns and message-passing concurrency. David works towards developing type-based techniques for implementing correct and predictable concurrent and distributed systems. He is interested in extending the notion of behavioural types for capturing constraints on the execution costs of concurrent systems. Most recently, David has been working on the development of a certified framework for implementing and verifying distributed systems in the Coq interactive theorem prover.
Olaf Chitil’s interests are connected to programming and programming languages. He is interested in semantics and theoretical foundations of programming languages, type theory, program transformation, compiler construction, message-passing-based concurrency, programming tools, and how to write programs. Olaf aims to support programmers in developing software more effectively. His favourite programming languages are functional languages, especially Haskell. Currently he is focusing on type error debugging and omniscient debugging. An omniscient debugger traces details of a program execution and then allows free navigation through the execution, including backwards and forwards.
Stefan Kahrs’ main research interests are various flavours of term rewriting, e.g. infinitary rewriting, higher-order rewriting, as well as the first-order case. These cover the whole range from implementations, proving properties about them, to semantic models. In recent years Stefan has been specialising on infinitary rewriting.
Stephen Kell is interested in improving the experience of programming, with a focus on infrastructure – which spans language designs, right the way down to operating systems and hardware. For Stephen, many of the most interesting issues are in the spaces between [conventional] languages: in language interoperability, debugging and live programming support, build and deployment systems, how we program I/O, infrastructure for testing and analysis, and the contract between programs and operating systems.
Stefan Marr is interested in programming language implementation techniques for concurrent and parallel programming. He believes that one of the biggest problems of today, is to use the already invented programming models in a safe way in the same application. Therefore, he is working on combining concurrency models in a safe manner. Stefan is also interested in helping developers to make sense of complex concurrent programs with appropriate tools, since concurrent systems are notoriously complex.
Dominic Orchard’s research centres on understanding and exposing the underlying structure in programming as a way to aid program verification. He often works at the intersection between formal logic, types, and semantics, using mathematics to capture and describe programming abstractions simultaneously across these three domains. This theoretical work informs the more practical aspects of his research, designing and building programming languages and tools. Dominic’s more applied research focusses on building lightweight verification tools for scientists.
Tomas Petricek is interested in finding easier and more accessible ways of thinking about programming. To do so, he combines technical work on programming languages and tools with research into history and philosophy of science. On the technical side, Tomas is interested in unorthodox ideas in programming language design such as integrating external data into type systems (type providers) or representing programs not as code, but as a sequence of interactions. On the philosophical side, he has been exploring the surprisingly rich nature of programming concepts such as types, monads and errors from the perspective of philosophy of science. He is also interested in finding and recovering good ideas in the history of programming that got lost for one reason or another.
David Castro-Perez‘s research interests are focused on the development and application of techniques for reasoning about functional (correctness) and extra-functional (e.g. execution costs) properties of systems, and the development of certified tools in dependently typed languages and theorem provers.