James Davenport and colleagues research topics
1. Formal Specifications of Analytic Functions
It is relatively easy to specify functions such as z^2 or exp(z) as functions from the complex numbers to the complex numbers. Even square root is harder to specify, and much harder to reason with, essentially due to the branch cut. Logarithms, or other functions defined by analytic continuation but subject to branch cuts, have never been formally defined as complex functions. This project will build on previous work of the supervisor and colleagues to produce such a formal definition framework, and tools for manipulating such definitions.
Further details and references.
2. Formal Statements of Pedagogic Correctness
It is possible to use the techniques of computer algebra, or of rewrite rules, to say whether or not two expressions A and B are mathematically equivalent. This, however, is a long way from saying whether, if A is the answer to a question posed in a textbook or an examination, B is also a correct answer. This question has bedevilled much computer testing, but is, we believe, capable of algorithmic answers.
Further details and references.
3. Block Cylindrical Decomposition
We may be able to use recent developments by Chris Brown to construct a more efficient Cylindrical Decomposition, that is only "cylindrical where necessary".
Further details and references.
4. Various Topics in Cryptography
These are not currently as well written-up. One topic of interest is what to do if/when the adversary has, or might have, a quantum computer and can therefore factor numbers and/or solve the discrete logarithm problem. See a recent workshop JHD was at.