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.

Researchers:

• Prakash Panangaden, Professor, McGill
• Brigitte Pientka, Assistant Professor, McGill
• Clark Verbrugge, Assistant Professor, McGill

Undergraduate Students:

• 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

Graduate Students (Masters and Phd):

• 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)

Collaborators and collegues:

Courses:

• 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
• COMP 762B:Computation and Deduction, Brigitte Pientka

[ Home | Researchers | Collaborators | Courses ]

bp@cs.mcgill.ca
Brigitte Pientka