I am interested in the use of simulation techniques, including agent-based simulation and virtual worlds, to understand real-world socio-economic phenomena. I am currently collaborating with Adam Kleczkowski from Mathematics on a project using agent-based simulation to model the effect of human behavioural changes on the spread of disease epidemics across a spatial network. Our models include consideration of the economic cost of behavioural changes (for example, if people stay home from work to avoid infection, there is cost to society), in relation to the economic benefit from reducing the size of the epidemic.
In previous work, I investigated the use of formal, mathematical techniques for the development of critical systems. Some specific areas of interest include: the use of theorem-proving tools, particularly those based on higher-order logics and type theory, for formal reasoning about specifications, programming languages and programs; the design and semantics of formal specification languages. I collaborated with Thomas Wilson and Robert Clark, on the Omnibus project. I have also worked with Carron Shankland and Muffy Calder on studying the symbolic semantics of the LOTOS specification language; with Juan Biccaregui on formalizing VDM within the PVS theorem prover; with Elsa Gunter on formalizing the semantics of Standard ML within the HOL theorem prover; with the Lego group at Edinburgh University; and with Edward Farrell of the University of the West Indies.