Research

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.

Security

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).