Olivier Savary BĂ©langer

Note: I have moved to Princeton for my PhD. Please follow this link to my new website for up-to-date information.


(Beluga) Caviar:

Together with Brigitte Pientka and Stefan Monnier, I worked 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. My masters thesis on the subject is available here. A paper describing the implementation appeared in the proceedings of CPP'13 and is available here.

(Abella) Automated Reasoning with Contexts Plugin

In 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. A paper describing the plugin and plugin framework has been published at LFMTP'14 and is available here. The code is on github.