Brigitte Pientka Assistant Professor McConnell Eng. Room 107N School of Computer Science McGill University 3480 University Street Montreal, Quebec, H3A 2A7 Canada phone: +1 (514) 398 2583 e-mail: bp at cs.mcgill.ca

My research interest lies in developing a theoretical and practical foundation for building and reasoning about reliable safe software systems. To achieve this goal, I combine theoretical research on the mathematical foundations of computer science in programming languages and verification with system building. The topics I am interested in include logics (classical and non-classical), type theory, theorem proving, logic and functional programming, and logical frameworks.

If you want to find out more, check out the Logic and Computation Group at McGill.

If you are looking for the SOCS outreach roadshow, you can download it here.

If you are looking for the Ugrad Research Opportunities at McGill see here.

Professional Activities:

• International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP'07), Bremen, Germany (Organizer, PC member).
• Programming Languages meets Program Verification (PLPV'07)(PC member)
• International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP'06), Seattle, USA (Organizer). An electronic version of the proceeding (pdf) is available.
• 22nd International Conference on Logic Programming (ICLP'06), Seattle, USA (Program committee member, Invited Tutorial Speaker)
• Area editor (Theorem Proving) for the Association of Logic Programming Newsletter
• ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS'06), Ottawa, Canada (Program committee member)
  

Selected Publications:

• Functional programming with higher-order abstract syntax and explicit substitutions, Brigitte Pientka, Programming Languages meets Program Verification (PLPV), August 21, 2006 (to appear)
  
• Overcoming perfomrance barriers: efficient verification techniques for logical frameworks, Brigitte Pientka, 22nd International Conference on Logic Programming (ICLP'06), August 17 - 20, 2006 (invited tutorial, to appear)
  
• Eliminating redundancy in higher-order unification: a lightweight approach, Brigitte Pientka, 3rd International Joint Conference on Automated Reasoning (IJCAR'06), August 17 - 20, 2006 (to appear)
  
• Contextual modal type theory, Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka, (56 pages, submitted Sept 2005, accepted May 2006) (a revised version will appear in ACM Transactions on Computational Logic)(ps)
  
• Small proof witnesses for LF, Susmit Sarkar, Brigitte Pientka, Karl Crary, 21th International Conference on Logic Programming, Barcelona, Spain, Springer-Verlag, 2005 (to appear) (ps)
  

• Tabling for higher-order logic programming, Brigitte Pientka, 20th International Conference on Automated Deduction, Talinn, Estonia, pages 54 -- 69, Springer-Verlag, 2005 (ps)
  See the new Twelf distribution with substantially improved tabling
  

• Verifying termination and reduction properties about higher-order logic programs (extended tech-report version), Brigitte Pientka, accepted in the Journal of Automated Reasoning (JAR) in a special issue on termination, Jan 2005
  

Current Courses:

• COMP 302:Programming Languages and Paradigms, Winter 2007
• COMP 426:Automated Reasoning, Fall 2006
• COMP 762:Computation and Deduction, Fall 2006