Olivier Savary-Bélanger
Graduate student in Computer Science, McGill University
Project Description
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.
Future work includes extending the source language to system
F and defining a notion of context subsumption in order to
reduce the number of explicit context relations.