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.