Generalised higher-order free extensions
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
The objective of this research is to leverage contemporary techniques from abstract algebra for the transformation and verification of computer programs and database queries. Rather than investigating specific programming / query languages from the outset and developing direct transformations thereof, this project considers the problem of transforming general programs abstractly in terms of free extensions of algebras.
Free extensions are used to characterise the terms / expressions of a language when extended by a collection of free variables or 'unknowns'. Therefore, by understanding the structure of free extensions, we gain insight into how we may manipulate expressions by rearranging or evaluating their sub-expressions, with the aim of obtaining equivalent, yet simplified / optimised, expressions. This ultimately improves the performance of program / query execution. Moreover, by carefully recording the steps taken while manipulating expressions, we can automatically derive proofs of the correctness of the transformations that have taken place - i.e., the meaning of the program / query is preserved.
While already well-understood for those languages described by standard universal algebra, this project aims to push the boundaries of our understanding by extending the family of language constructs that can be modelled using free extensions. We are particularly interested in dependent types, binding operators and differential operators.
This abstract approach is valuable as it is backed by a strong abstract characterisation of the problem it solves. As such, the tools and techniques developed as part of this project are highly reusable. That said, the methods this project aims to develop have many direct applications in compiler construction, incremental computation and formal verification.
This project is partially funded by GitHub through an iCASE studentship due to its potential applications in their general purpose static analysis system 'CodeQL', responsible for statically checking security properties for large volumes of source code. In particular, the CodeQL project is interested in the derivation and verification of procedures for the symbolic differentiation of relational query languages in order to support efficient incremental evaluation of their analyses. Efficient evaluation of relational expressions sits at the heart of the CodeQL evaluator and is essential for providing critical analysis results in a timely fashion. Incrementalising this system has the potential to bring drastic performance improvements, giving developers access to immediate feedback on a commit-by-commit basis.
This project falls within the EPSRC programming languages and compilers research area.
Free extensions are used to characterise the terms / expressions of a language when extended by a collection of free variables or 'unknowns'. Therefore, by understanding the structure of free extensions, we gain insight into how we may manipulate expressions by rearranging or evaluating their sub-expressions, with the aim of obtaining equivalent, yet simplified / optimised, expressions. This ultimately improves the performance of program / query execution. Moreover, by carefully recording the steps taken while manipulating expressions, we can automatically derive proofs of the correctness of the transformations that have taken place - i.e., the meaning of the program / query is preserved.
While already well-understood for those languages described by standard universal algebra, this project aims to push the boundaries of our understanding by extending the family of language constructs that can be modelled using free extensions. We are particularly interested in dependent types, binding operators and differential operators.
This abstract approach is valuable as it is backed by a strong abstract characterisation of the problem it solves. As such, the tools and techniques developed as part of this project are highly reusable. That said, the methods this project aims to develop have many direct applications in compiler construction, incremental computation and formal verification.
This project is partially funded by GitHub through an iCASE studentship due to its potential applications in their general purpose static analysis system 'CodeQL', responsible for statically checking security properties for large volumes of source code. In particular, the CodeQL project is interested in the derivation and verification of procedures for the symbolic differentiation of relational query languages in order to support efficient incremental evaluation of their analyses. Efficient evaluation of relational expressions sits at the heart of the CodeQL evaluator and is essential for providing critical analysis results in a timely fashion. Incrementalising this system has the potential to bring drastic performance improvements, giving developers access to immediate feedback on a commit-by-commit basis.
This project falls within the EPSRC programming languages and compilers research area.
People |
ORCID iD |
| Luke Ong (Primary Supervisor) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/T517811/1 | 01/10/2020 | 30/09/2025 | |||
| 2711688 | Studentship | EP/T517811/1 | 01/10/2021 | 31/03/2025 |