Dr Andrei Popescu, member of the Security of Advanced Systems (SoAS) research group and the Foundations of Computation (FOX) research groups, has received distinguished paper awards at the last three POPL (Principle of Programming Languages) conferences.
POPL is one of the most prestigious conferences in Computer Science, a forum for the discussion of all aspects of programming languages and programming systems.
The three papers are:
- 2023 – Admissible Types-to-PERs Relativization in Higher-Order Logic (co-authored with Dmitriy Traytel)
- 2024 - Nominal Recursors as Epi-Recursors
- 2025 - Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings (co-authored with Jan van Brügge, James McKinna and Dmitriy Traytel)
The best paper awards were given for work on formal reasoning principles, with applications to the design and implementation of proof assistants.
Andrei's work on the foundations of proof assistants is often applied to the development of a popular system called Isabelle, which is used for research by academics from the FOX group. It has formed the basis of several PhD theses and research grants in the FOX and SoAS research groups
Andrei said: "I am truly honoured and humbled by these awards. They come in the context of increasing recognition of proof assistant research within the broader areas of programming languages and formal methods.
"Proof assistants, also known as interactive theorem provers, are interactive tools used for the specification and verification of software and hardware systems, and for the formal certification of mathematical theorems. For example, what makes us sure that a critical system, such as a power grid controller, will operate without flaws? Testing is usually effective for detecting errors, but can almost never guarantee that all errors have been caught. Proof assistants are deployed to address this via comprehensive machine checked mathematical proofs that systems behave correctly.
"The above mentioned papers study inductive reasoning and transfer principles that allow researchers to write their proofs in a more hassle-free manner, enabling powerful automation support from the theorem proving engine. They build upon concepts from Nominal Logic, a versatile theory of names and bindings.”