Compositionality is a trait that is inherent to both mathematical proofs and programs. Just like mathematical reasoning is conducted from axioms and is organised via lemmas and theorems, with the details of the proofs abstracted away, good programs are structured via functions, modules, and objects, hiding the details of the implementations. This structure is what makes software development scalable and tractable. However, compositionality (and, hence, scalability and tractability) is tricky to get right in the cases when programming meets proving—a situation that takes place naturally once one tries to formally verify that a program is correct with respect to an ascribed specification (a mathematical statement), and then use this specification to verify programs built on top of that one.

In my talk, I will describe my journey to date towards building techniques for scalable computer-assisted verification of correctness-critical programming artefacts, focusing specifically on programs with “interesting” features, such as concurrent and distributed computations. I will show how a combination of type theory, program logics, and semantics—all standard working tools of a programming languages researcher—enables construction and composition of provably correct software systems.

I am an Associate Professor (without tenure) at Yale-NUS College and School of Computing, NUS (Singapore).

Prior to joining Yale-NUS, I was a a faculty at University College London. Before then, I was a postdoctoral researcher at IMDEA Software Institute (Madrid, Spain). I defended my PhD in 2012 in the DistriNet research group at the Department of Computer Sciences of KU Leuven (Belgium). Before that I received my MSc degree in Mathematics and Computer Science from Saint Petersburg State University (Russia) in 2008.

My research interests dwell in the area of the design and implementation of programming languages, including but not limited to program semantics, certified programming, concurrency and abstract interpretation. I am particularly interested in developing verification techniques and static analyses for higher-order and concurrent programs.