My research is at boundaries between programming languages, system programming, and computer architectures, with the overall goal of producing systems which are better-understood, more robust, and more secure. Below is a short overview of my main projects.

On the Hack language

I have extended Meta's Hack language and runtime to make it a better fit for Meta's large framework use cases. In particular I designed and implemented:
  • lightweight dependent types to encapsulate database accesses with uniform typed getters and setters;
  • partial classes to split large classes among multiple files;
  • safe support for trait diamond inheritance;
  • friend modules;
  • fast method call tracing and mocking.

On debug information

DWARF is a widely-used debugging data format. DWARF is obviously relied upon by debuggers, but it plays an unexpected role in the runtime of high-level programming languages and in the implementation of program analysis tools. The debug information itself can be pervaded by subtle bugs, making the whole infrastructure unreliable. I am currently investigating techniques and tools to perform validation and synthesis of the DWARF stack unwinding tables, as well as working on adventurous projects that can be built on top of reliable DWARF information.

Weak memory models

Multiprocessors are now pervasive but typical multiprocessors (x86, Sparc, Power, ARM, Itanium) and programming languages (C, C++, Java) do not provide the sequentially consistent shared memory that has been assumed by most work on semantics and verification. I worked to develop mathematical semantics for multiprocessor programs, focussing on the x86 processor architecture and on the C and C++ languages, and on reasoning and verification using these models. In particular with Owens, Sarkar, and Sewell, I defined the de-facto standard x86-TSO memory model of the x86 architecture. With Jagannathan, Sewell, Sevcik, and Vafeiadis, I studied the verified compilation of a concurrent dialect of the C language to the x86 architecture. I also supervised the PhD thesis of Morisset, in which we studied the correctness of compiler optimisations in the C and C++ memory models, and developed a tool, cmmtest, to perform random testing of mainstream compilers.

Programming language design

With Belyakova, Chung, Pelenytsin, Vitek, and the help of Jeff Bezanson, I have reverse engineered the amazing subtype algorithm at the heart of Julia's multiple dispatch, provided its first formal specification, and built a reference implementation that can be relied upon for differential testing.

With Vitek and Wrigstad I designed Like types, a novel gradual type system for dynamic languages. In contrast to previous proposals, this approach captures common programmer mistakes, is compatible with object-orientation and can be implemented efficiently. Initially implemented in the Thorn programming language, and with Richards, in the StrongScript dialect of JavaScript. It is today supported by Meta's Hack language.

With Appel and Hobor I started the Concurrent C Minor project, whose goal was to study techniques to prove the correctness of realistic implementations of concurrent shared-memory algorithms.

Previously, with Leifer, Sewell and Wansbrough, I developed principled support for type-safe interaction between distributed programs. These ideas were realised in the Acute prototype language.


While working at the MSR-Inria Joint Centre, I supervised Guts PhD, on the formal properties of audit logs. The main contribution (with Fournet) is an algorithmic method based on types with logical refinements to verify if a protocol implementation collects enough evidence to prove a posteriori properties about each protocol run.

Tool-support for semantics

Precise definitions of programming languages are needed, but the available metalanguages for expressing semantics make it much harder than necessary to work with large definitions. With Sewell and Owens I designed a metalanguage and implemented a tool, Ott, to specifically address this problem.

Process languages

My early work focused on proof techniques for higher-order process languages (with Merro) and denotational models for concurrency and name generation (with Winskel).

A few recorded talks

C Concurrency: Still Tricky: Keynote at EuroLLVM 2015.

Debugging Debug Information and Beyond: ETH WSCR 2017.

Subtyping Made Simple: JuliaCon 2018.

PhD students

Basile Clement: Machine Learning for Synthesis of High-Performance Numerical Libraries, started in Sept. 2018, then supervised by Xavier Leroy.

Robin Morisset: Compiler Optimisations and Relaxed Memory Consistency Models, 2017.

Nataliya Guts: Auditability for Security Protocols, 2011.


Program Committees

PC Member: POPL 2023, OOPSLA 2019, ECOOP 2017, POPL 2017, PPoPP 2015, ESOP 2015, POPL 2012 (also JFLA 2017, JFLA 2008).

ERC Member: ECOOP 2016, OOPSLA 2014, POPL 2013.

Last update: