People
Faculty
Graduate Students
- Jacob Errington, MSc student, "Mechanize Proofs Now!"
- Aliya Hameer, MSc student, "POPLMark Reloaded: Mechanizing Logical Relations Proofs"
- David Thibodeau, PhD student, "Programming coinductive proofs"
Past Postdocs
- Mathieu Boespflug(PhD École Polytechnique, France, January 2011 - Dec 2012), Beluga modulo
- Joshua Dunfield (PhD Carnegie Mellon University, September 2007 - August 2010), "Programming and reasoning with higher-order data"
- Levi Lucio (PhD University of Geneva, Switzerland, August 2011 - August 2014, jointly supervised with Prof. Hans Vangheluwe), "Modelling and reasoning about automotive software"
- Matthias Puech (PhD University of Bologna, Italy, April 2014 - April 2014), "Logical foundation for open code generation"
- Tao Xue (PhD University of London, UK, June 2012 - August 2013), "Proof-carrying authorization in Beluga"
Graduate Alumni
- Francisco Ferreira, PhD 2018, "Proofs and Programs about Open Terms"
- Rohan Jacob-Rao, MSc 2017, "Well-founded Recursion in Terms and Types"
- Stefan Knudsen, MSc 2017, "Dependently Typed Reactive Programming"
- Andrew Cave, ABD 2017, "Programming and reasoning with proofs"
- Olivier Savary-Bélanger, MSc 2014, "Programming type-safe transformations using higher-order abstract syntax"
- Shawn Otis, MSc 2017, "A Linear Logical Framework with First-Class Contexts"
- Samuel Gélineau, MSc 2010, "Commutative composition - a conservative approach to aspect weaving"
- Renaud Germain, MSc 2010, "Implementation of a dependently typed functional programming language"
- Ian Clément, MSc 2008, "Proof theoretical foundations for constructive description logic"
- Samuli Heilala, MSc 2009, "A path characterization of validity for multimodal logics"
- David Xi Li, MSc 2007, "Focused inverse method for logical frameworks"
- Jacques Le Normand, MSc 2007,
"Guarded abstract data-types"
- Ahmer Ahmedani, MSc 2006, "Information flow in a Java intermediate language"
- Ye Henry Tian, MSc 2005, "Mechanically verifying correctness of CPS compilation"
Undergraduate Alumni
- Aina Linn Georges, "Mechanizing Lincx: a linear logical framework with first-class contexts", 2016
- Theophile Gervet, "Producing human-readable proofs", Summer 2016
- Elizabeth Sulmont, Winter 2016
- Sherry Shanshan Ruan, "Well-founded recursion over contextual objects and contexts", 2013, SURA Award
- Steven Thephsourinthone, "Producing human-readable proofs", Summer 2013
- Esma Balkir, "Coinductive reasoning", Autumn 2012, Honors student project,
- Gabriel Gaudreault, "Linear contextual logic", Honors student project, Summer 2012
- Marie-Andrée Langlois, "A user friendly interface to Beluga", "SasyBel: Interactive proof tutor for Beluga", 2011-2012
- Costin Badescu, "Implementing a higher-order logic programming interpreter", "Structural termination checking for contextual objects", 2011-2012, NSERC USRA
- Rafik Draoui, "Size based termination", Summer 2011
- Shen Chen Xu, "Coverage checking for dependently typed programs", Winter 2011, Honors thesis
- Stephane Bersier, "Programming with contexts—a tutorial", Winter 2010
- Andie Sigler, "Programming with contexts—a tutorial", Winter 2010
- Ali Assaf, "An environment-based semantics for Beluga", Science Undergraduate Research Award, honorable mention for outstanding male undergraduate at the Computing Research Association
- Abbie Desrosiers, "Compiler construction with higher-order abstract syntax", Summer 2009, Honors Theses
- Benjamin Azan, "Type systems for Featherweight Java: Theory and Implementation", Summer 2005, winner of the SoCS Undergraduate Research Excellence Prize
- Sabrina Chantrelle, "Focusing prover for bunched implications", Summer 2005
- Maja Frydrychowicz, "A logical foundation for enforcing access control", Summer 2007, "Termination checking when programming with proofs", Summer 2008, runner-up of the SoCS Undergraduate Research Excellence Prize, honorable mention for outstanding female undergraduate at the Computing Research Association, Canadian Distributed Mentoring Award,
- Andrés Franceschi Larrea, "A practical comparison between Twelf and LambdaProlog", Summer 2007, Science Undergraduate Research Award
- Daniel Pomerantz, "Forward proof search for intuitionistic modal logic", Summer 2006
- Dustin Wehr, "Refinement types for logical frameworks", "Practical programming with higher-order abstract syntax", 2007, Honors Theses
Past Visitors
Collaborators and Colleagues