Publications
Master's dissertation (in french): Certification de validateurs de tranformation
Jean-Baptiste Tristan and Xavier Leroy. Formal Verification of Translation Validators. A Case Study on Instruction Scheduling Optimizations. In 35th symposium Principles of Programming Languages. pdf
Research projects
-
Compcert
The compcert project aims at developping a certified optimizing compiler using the Coq proof assistant. It compiles a fair subset of the C language down to PowerPC assembly. It is leaded by Xavier Leroy . -
C--
The C-- project aims at developping a portable assembly language together with its compiler and a generic runtime system. It is leaded by Norman Ramsey