David Thibodeau

I am currently finishing a Joint Honours in Mathematics and Computer Sciences In January 2013, I will be starting a master's degree in computer science at McGill university under the supervision of Prof. Brigitte Pientka.

In summer 2011, I was working in the Logic and Computation Group under the supervision of Prof. Brigitte Pientka. In the first part of my project, I implemented several type checkers for different type systems such as simply typed lambda calculus, dependently typed lambda calculus and a pure type system that can emulate the lambda cube. In the second part of the project, I am studying the hereditary substitution, its implementation on my pure type system and the question of the termination of the hereditary substitution for type systems such as mine or System F. I will soon put a page presenting my project in more details.

This website is still in construction. I would need to do some design or at least find a template for it. It should be filled out soon.