About Us

Our research interests lie in developing a theoretical and practical foundation for building and reasoning about reliable, safe software systems. To achieve this goal, we combine theoretical research on the mathematical foundations of computer science with system building.

Some of the theoretical topics we focus on include classical and non-classical logics, type theory, verification, proof theory, analysis and design of programming languages, logic and functional programming, logical frameworks, and theorem proving.

We welcome applications from prospective graduate students, preferably students who are interested in pursuing a PhD. If interested, please contact Prof. Brigitte Pientka directly for more information and research interests.

Our research is funded by the Natural Sciences and Engineering Research Council of Canada (NSERC), Le Fonds québécois de la recherche sur la nature et les technologies (FQRNT), the Canada Foundation for Innovation (CFI) and McGill University.

Announcements

Beluga

Beluga is a functional programming language designed for reasoning about formal systems. It features direct support for object-level binding constructs using higher order abstract syntax and treats contexts as first class objects. For more information see the project page.

Contact Information

Individual group members may be reached through their respective homepages.