Undergraduate Summer Research (2009)

I spent last summer working with Brigitte Pientka at McGill University on Beluga, a functional programming language which supports Higher Order Abstract Syntax (HOAS).

HOAS is a useful technique for representing variable binders in the abstract syntax tree of an object language. However, it is inconvenient to use with current functional programming languages because they restrict us to work with closed terms.

Beluga supports programming with open terms. For example, we can view 1 + x as having type nat[x:nat], meaning that it has the type nat in the context where x is of type nat. This is based on contextual modal type theory, which corresponds to modal logic. It also supports dependent types, specifically the LF framework. With that, we can express, and prove, numerous properties about programs and logics.

I worked mainly on the operational semantics of the language. After familiarizing myself with the theory, I participated in the design of the evaluation rules.

Zerosudoku (2008)


I developped this Sudoku program for an online competition. I wrote it in C++, using the Qt toolkit for GUI. It ranked 4th out of 46.


The program is open source. You can download the source code, but remember that you need the Qt development libraries to compile it. Bare in mind that the project is not completely finished yet, and some features are still missing, but the implemented part is working and you'll find that the code is extensively commented.

Project page