Portrait of Olivier

Olivier Savary Bélanger

PhD student in Computer Science



  • Summer 2016 - I did an internship at Microsoft Research Redmond under the supervision of Nikhil Swamy and Leonardo de Moura. The internship centered on using Lean instead of Z3 to discharge verification conditions arising from type-checking F* terms.
  • Fall 2014 - I have joined the CertiCoq project! I am working on formal verification of efficient transformations over functional languages.

About Me

I'm PhD student in Computer Science at Princeton University, working with Prof. Andrew Appel on certified compilation of functional languages. Before moving to New Jersey, I studied (B.Sc, M.Sc.) at McGill University, Montreal, Canada. At McGill, I worked with Prof. Brigitte Pientka on type-preserving code transformations over object languages encoded with HOAS and with Prof. Laurie Hendren on compiling dynamic scientific languages such as MATLAB.

More details about my life are included in my résumé.



I'm currently working on CertiCoq, a verified compiler for Coq. Stay tuned for more information about this project soon!


A list of my publications is available here


  • I co-founded the Princeton Graduate Board Game Club in spring 2015. We meet every Saturday evening in the Old Graduate College. Join us if you are on campus! For more info, have a look at our facebook group .
  • For two years, I was a member of the Student Ambassors of Princeton University Concerts, centering my effort on promoting graduate student attendance to classical music concerts on campus.