• Programming Language Design
  

  The team works on high-level programming languages constructs that can both help programmers write programs without bugs and help compilers generate more efficient code. We are particularly interested in parallel programs, but also provide tools for sequential code.

• Semantics and Proofs

  Interactive provers like Rocq allow writting machine-checked mathematical proofs, and also in certified computer programs. We work both on tools for writting better proofs or formalization of semantics, and on the application of these tools in particular for certified compilation.

• Program Analysis and Verification
  

  We design expressive and scalable static analyses. The analyses we design both apply to performance optimization (by computing invariants used by optimizing compilers) and safety (by automatically finding bugs or proving correctness properties on programs or electrical circuits).

• Optimizations and Program Transformations
  

  We propose several automatic program transformations to improve their performance. On framework of particular interest to the team is the polyhedral model able to perform very agressive optimizations for regular imperative programs.

Main collaborations: XtremLogic, Aniah, and several academic compiler teams (Colorado State Univ (US), Univ of Mineas Gerais (Brasil)