PLAS Research Interests
The Research Interests of the Programming Languages and Systems research group are listed by the interests of individual members.
I develop 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). My 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.
My research spans several areas, which include software engineering, concurrency and formal methods. I am interested in theories and tools for developing safe distributed systems. I am 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, I have 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.
All my research interests are connected to programming and programming languages. I am 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. I aim to support programmers in developing software more effectively. My favourite programming languages are functional languages, especially Haskell. Currently I focus 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.
I am interested in software engineering for self-adaptive systems which involves the dynamic generation of processes and making systems and ensuring resilience. My background is in fault-tolerance and I am interested in designing architectural abstractions as well as validating dependable software architectures. Recently I have been investigating self-adaptive authorization for managing threats that come from inside an organisation.
I am interested in program analysis, runtime verification, and programming languages in general. In program analysis, I worked on tools based on verification condition generation, based on separation logic, or implemented in Datalog. In runtime verification, I worked on establishing links with the theory of nominal automata. In the general area of programming languages, I looked at the decidability of type systems. I enjoy working on highly technical problems stemming from program verification, preferably involving probabilities, boolean functions, and graphs.
My chief area of interest is dynamic memory management - this grew out of work on lazy functional programming languages and particularly their efficient implementation. My work spans from theoretical studies for example formalizing distributed reference counting and arguing its correctness to engineering concerns such as heat visualization and how to undertake rigorous and repeatable experiments in the context of benchmarking and particular memory management.
My 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 I have been specialising on infinitary rewriting.
My interests range from high-level declarative programming to low-level assembly code. A reoccurring theme of my work is abstract interpretation in which all paths through a program are systematically examined so as automatically derive information for optimising a program for, say, time or energy. Abstract interpretation is also increasingly used to search a program for bugs, such as security holes, which another interest of mine. Recently I have been working on geometric algorithms, reverse engineering and malware.
My research interests are centered on developing mathematically grounded theories and tools to support the specification and development of concurrent and distributed systems. In particular, I develop theories based process calculi, behavioural types, automata theory, and model checking to specify and verify message-passing oriented programs written in, e.g., Go, Erlang, Scala, etc.
I am interested in programming language implementation techniques for concurrent and parallel programming. One of the biggest problems of today is to use the already invented programming models in a safe way in the same application. Therefore, I am working on combining concurrency models in a safe manner. Since concurrent systems are notoriously complex, I am also interested in helping developers to make sense of complex concurrent programs with appropriate tools.
My research centres on understanding and exposing underlying structure in programming as way to aid program verification. I often work 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 my research, designing and building programming languages and tools. My more applied research focusses on building lightweight verification tools for scientists.
My research focuses on understanding and describing computer hardware and programming languages to enable rigorous and trustworthy software verification. Precisely and unambiguously capturing the intricacies of these artifacts invariably requires the language of formal mathematics. To this end, I use techniques drawn from the interactive theorem proving and programming languages communities.
My main research interests are in functional programming in Haskell, Erlang and OCaml. Most recently I have worked on refactoring tools for Erlang and Haskell, and our team are now building a trustworthy refactoring tool for OCaml; separately we are looking at languages for smart contracts on blockchain, and ways of making Erlang programming more secure through involving advanced type systems. I try to involve industry partners in my research: currently collaborations include Jane Street Capital, IOHK and Erlang Solutions. I have also worked in reasoning and multimedia.
I believe many problems in software engineering can and can only be solved by better programming languages, and better ways of using them. A recurring theme of my research is to guarantee correctness of program properties through construction, reasoning and testing. Functional languages with many of their distinctive features are well suited for the task and have been the main target and carrier of my research. Some of my recent topics involve designing languages for bidirectional transformations and property-based testing.