Olivier Savary-Bélanger

M. Sc. student in Computer Science, McGill University
  • Résumé (PDF)
  • osav...@cs.mcgill.ca


(Beluga) Caviar:

Together with Brigitte Pientka and Stefan Monnier, I am working on a type-preserving compiler in Beluga, a dependently-typed proof and programming environment with support for higher-order abstract syntax (HOAS). We currently have CPS, closure conversion and hoisting implemented over STLC. A paper describing the implementation appeared in the proceedings of CPP 2013.

(Abella) Automated Reasoning with Contexts Plugin

This summer (2013), I worked with Kaustuv Chaudhuri on symplifying reasoning with contexts in Abella by providing a mechanism for declaring contexts with regular structure and automatically generating theorems on properties that always hold for contexts defined using our facilities. The internship report is available here, and the code is available on github. A paper draft on the subject will appear here soon.