The University of Kent, Canterbury, Kent, CT2 7NZ, T +44 (0)1227 764000
Writing bug-free software is difficult. The correct operation of any particular program relies on the hardware and software systems that it interacts with. However, we all too often have only a vague idea of how these systems behave. This is especially the case for concurrent programs designed to take advantage of modern multi-core processors, which often have fiendishly non-intuitive memory systems.
My research focuses on understanding and describing computer hardware and programming languages to enable rigorous and trustworthy software verification. Precisely and unambiguously capturing the intricacies of these artifacts invariably requires the language of formal mathematics. To this end, I use techniques drawn from the interactive theorem proving and programming languages communities.
Summer School on Types and Programming Languages (June 7 - June 9, 2012)