Research

(back)

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.

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.

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.

Programming language design

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, it later evolved, with Richards, in the StrongScript dialect of JavaScript.

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.

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

Grants

ANR-11-JS02-011 WMC (2012-2016), Google European Fellowship in Operating Systems (Robin Morisset), 2013-2016, ANR-06-SETIN-010 ParSec (2007-2010), INRIA Associate Teams MM.


Program Committees

PC Member: 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: