David's research is on applying programming language-based techniques to the development of safe and predictable systems, with a strong emphasis on concurrent and distributed systems. In these areas, I develop and apply techniques based on behavioural types for reasoning about functional (e.g. correctness) and extra-functional (e.g. cost) of concurrent and distributed systems. I developed high-level frameworks for parallel programming that provide guarantees of correctness by construction, and I developed static cost analysis for predicting the potential achievable speedups. Additionally, I am very interested in build certified tools and languages, mostly in (but not limited to) the Coq interactive theorem prover.
I am a member of the following research groups:
Broadly speaking, my research interests are focused on the development and application of techniques for reasoning about functional (correctness) and extra-functional (e.g. execution costs) properties of systems, and the development of certified tools in dependently typed languages and theorem provers.