Short About

Brigitte Pientka is an Associate Professor in the School of Computer Science at McGill University, and leading the Computation and Logic group. She received her PhD from Carnegie Mellon University in 2003, and studied previously at the University of Edinburgh and Technical University of Darmstadt.

Sidebar Menu

Home
Research Interests
Recent Publications
Professional Activities

Research Interests

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 logical 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.

For more information, you can visit Computation and Logic group.

As part of CSEdWeek, I recently gave a talk on "Computational Thinking!". Comments are welcome.

Recent Publications

Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records, accepted at TLCA'11. (long version)
Brigitte Pientka. Programming proofs: A novel approach based on contextual types (submitted, 1 Feb 2011)
Brigitte Pientka and Joshua Dunfield. Covering all bases: design and implementation of case analysis for contextual objects. technical report, Oct 2010. (pdf, electronic appendix, electronic appendix (tar-ball))
An insider's look at LF type reconstruction:Everything you (n)ever wanted to know, Brigitte Pientka, (submitted, Aug 2010)
Programming inductive proofs: a new approach based on contextual types, Brigitte Pientka, Verification, Induction, and Termination analysis, LNAI, Springer, Aug 2010
Explicit substitutions for contextual type theory, Andreas Abel and Brigitte Pientka, International Workshop on Logical Frameworks: Theory and Practice (LFMTP'10), July 2010(Implementation of the type checker in Haskell )
Beluga: programming with dependent types, contextual data, and contexts,Brigitte Pientka, Invited talk at 10th International Symposium on Functional and Logic Programming (FLOPS'10), April 2010, Sendai, Japan.
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison,Amy Felty and Brigitte Pientka, to appear at ITP'10 (Electronic Appendix (pdf, mechanized proofs and examples), July 2010
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System description),Brigitte Pientka and Joshua Dunfield, to appear at IJCAR'10, July 2010
Higher-order term indexing using substitution tree, Brigitte Pientka, ACM Transactions on Computational Logic, Vol 11, issue 1 (October 2009).
Programming with proofs and explicit contexts, Brigitte Pientka and Joshua Dunfield, 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), ACM Press, 2008
Case analysis on higher-order data, Joshua Dunfield and Brigitte Pientka, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08), 2008
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, Brigitte Pientka, 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pages 371-382, ACM Press, 2008.
Contextual modal type theory, Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka, (60 pages), ACM Transactions on Computational Logic, vol 9, number 3, 2008.

For a list of all publications see Research.

Software release

Beluga Version 0.3 (7 Oct 2010) (includes type reconstruction, supports context subsumption, provides an interpreter and coverage checker)
Tutorial on how to write some advanced examples in Beluga

Professional Activities

Invited Talk

Beluga: programming with contextual data, contexts, and ... , Brigitte Pientka, Invited talk at Programming Languages for Mechanized Mathematics Systems (PLMMS'10), July 2010, Paris, France
Beluga: programming with dependent types, contextual data, and contexts, Brigitte Pientka, Invited talk at 10th International Symposium on Functional and Logic Programming (FLOPS'10), April 2010, Sendai, Japan.

Conference Chair

22nd International Conference on Automated Deduction (CADE'09)

Editor

Guest Editor for a special issue in Journal of Automated Reasoning for the best papers of CADE-22 (Co-editor with Renate Schmidt)
Guest Editor for a special issue in Information and Computation on Intuitionistic Modal Logics and Applications (IMLA) (Co-editor with Valeria de Paiva)
(call for papers, deadline: May 31, 2009)

Program Committee

CiE 2012: Turing Centenary Conference: How the world computes, Cambrigde, England (PC)
39th ACM Symposium on Principles of Programming Languages (POPL 2012), Extended Review Committee
First International Conference on Certified Programs and Proofs (CPP 2011), co-located with APLAS'11, Taiwan, Dec 2011
International Conference on Interactive Theorem Proving (ITP'11), Nijmegen, Netherlands, Aug 2011
23rd International Joint Conference on Automated Deduction (CADE-23), 2011, Waslaw, Poland, July 2011
5th International Joint Conference on Automated Reasoning (IJCAR-10)
International Conference on Interactive Theorem Proving (ITP-10)
26th International Conference on Mathematical Foundations of Programming Semantics (MFPS) (MFPS-10)
19th International Workshop on Functional and (Constraint) Logic Programming (WFLP'10)
22nd International Conference on Automated Deduction (CADE'09)
International Workshop on Proof-Search in Type Theories (PSTT'09)
7th International Workshop on the Implementation of Logics (IWIL'08)
13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08)
24th International Conference on Logic Programming (ICLP'08)
International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP'08)

Professional Organizations

Elected Trustee of Conference of Automated Deduction (CADE)
Steering Committee of Logical Frameworks and Meta-Languages (LFMTP)