Logic and Computation Group
Our research interest lies 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 include classical and non-classical logics, type theory, verification, proof theory, analysis and design
of programming languages, logic and function programming, concurrency,
pi-calculus, logical frameworks, theorem proving and category theory.
Our research is funded by the National Science and Engineering
Research Council of Canada (NSERC), Fonds Quebecois de la recherche sur la nature et les technologies (FQNRT), the Canadian Foundation of Innovation and McGill University
We welcome applications from prospective graduate students, preferably students who are interested in pursuing a PhD. Please contact the individual faculty members for more information.To find out about the interests of individual faculty members, you can follow the links to their home pages.
- Benjamin Azan, "Type systems for Featherweight Java: Theory and Implementation"
(Winner of the best undergraduate research project 2005)
- Sabrina Chantrelle, "A focusing prover for bunched implications" (Stage project), Summer 2005
- David Xi Li, "Decision Procedures for propositional logic and congruence closure", Summer 2005
- Samuli Heilala, "Proof search in intuitionistic modal logic" (Honors Project), Summer 2006
- Daniel Pomerantz, "Forward proof search for intuitionistic modal logic", Summer 2006
- Maja Frydrychowicz, "A logical foundation for enforcing access control", Summer 2007
- Dustin Wehr, "Managing a digital library : Exploring retrieval strategies for lemma selection ", Summer 2007
- Ye Henry Tian, "Mechanically verifying correctness of cps-translation" (graduated in 2005)
- Ahmer Ahmedani, "Statically verifying information flow" (graduated in 2006)
- David Xi Li,"Forward theorem prover for logical frameworks"
- Jacques Le Normand, "Guarded abstract data-types"
- Samuli Heilala (Modal logic and modal type systems)
- Renaud Germain (to be announced)
Universite de Montreal
Carnegie Mellon University
- COMP 426:Automated
Reasoning, Brigitte Pientka
- COMP 523:Language-based Security, Brigitte Pientka
- COMP 524:Programming Language Theory, Prakash Panangaden
- COMP 525:Formal Verification, Prakash Panangaden
- COMP 527:Theory of Programing Languages, Prakash Panangaden
762B:Computation and Deduction, Brigitte Pientka