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.
Projects
(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.