Research
A list of publications is available here. Tools developed as part of my research can be downloaded from this page.
More information on my research is available at my Oxford Computing Laboratory webpage.
The safe lambda calculus
This is the topic of my PhD. See my DPhil transfer report for more information on the subject.
Termination analysis
This line of research was pursued during my Master in Computer Science (2004).
Lee, Jones and Ben-Amram introduced "size-change termination", a
decidable property strictly stronger than termination. They invented a
method called the "size-change principle" to analyze it.
Based on the work of Jones and Bohr, I propose an extension of the size-change principle to a subset of ML
featuring ground type values, higher-order type values and recursively
defined functions. Compared to other works, this is the first time
that the size-change principle is
applied to a higher-order functional language.
The language handles natively if-then-else and let rec structures. The
resulting algorithm produces the expected result for higher-order
values but can also analyze the size of ground type values. This
enhances the scope of the termination analyzer to some recursively
defined function operating on numbers.
