Skip to content. Skip to navigation
McGill Home SOCS Home
Personal tools
You are here: Home People Profile

Brigitte Pientka


photo

Email: bp AT cs DOT mcgill DOT ca
Home Page: http://www.cs.mcgill.ca/~bpientka
Office: MC107N
Phone: +1-514-398-2583
Fax: +1-514-398-3883
Address:

Research Description

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.

Research Interests

Research Labs

Teaching

Selected Publications (click link in front of each publication to see bibtex in ASCII format)

[1] Pientka, B. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In 35th ACM Symposium on Principles of Programming Languages (POPL'08),. ACM Press, January 2008, pp. 371-382.
[2] Pientka, B., and Dunfield, J. Programming with proofs and explicit contexts. In ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08). ACM Press, July 2008, pp. 163-173.
[3] Nanevski, A., Pfenning, F., and Pientka, B. Contextual modal type theory. ACM Transactions on Computational Logic, 2008, v. 9, n. 3, pp. 1-49. Nanevski:ICML05.
[4] Pientka, B. Higher-order term indexing using substitution trees. ACM Transactions on Computational Logic, 2008, pp. 1-50. Pientka:TOCL08 In Press.
[5] Pientka, B. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08). ACM, 2008, pp. 371-382. Pientka:POPL08.
[6] Pientka, B., and Dunfield, J. Programming with proofs and explicit contexts. July 2008, pp. 163-173. Pientka:PPDP08.
[7] Heilala, S., and Pientka, B. Bidirectional decision procedures for the intuitionistic propositional modal logic is4. In Pfenning, F., editor, 21st International Conference on Automated Deduction (CADE-21), Bremen, Germany, July 17-20, 2007. Springer, 2007, v. 4603 of Lecture Notes in Computer Science, Lecture Notes in Computer Science, pp. 116-131.
[ http ]
[8] Pientka, B. Proof pearl: The power of higher-order encodings in the logical framework LF. In Schneider, K., and Brandt, J., editors, 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'07), Kaiserslautern, Germany. Springer, 2007, Lecture Notes in Computer Science (LNCS 4732), pp. 246-261.
[9] Pientka, B. Functional programming with higher-order abstract syntax and explicit substitutions. Electronic Notes Theoritical Computer Science, 2007, v. 174, n. 7, pp. 41-60.
[ http ]
[10] Momigliano, A., and Pientka, B. Proceeding of the international workshop on logical frameworks and meta-languages: Theory and practice (lfmtp'06), seattle, wa, usa. Electronic Notes Theoretical Computer Science(ENTCS), 2007, v. 174, n. 5, pp. 1-2.
[ http ]
[11] Nanevski, A., Pfenning, F., and Pientka, B. A contextual modal type theory. ACM Transactions on Computational Logic, 2006, p. 56. In Press.
[12] Pientka, B. Overcoming performance barriers: Efficient verification techniques for logical frameworks.(invited tutorial). In Etalle, S., and Truszczynski, M., editors, 22nd International Conference Logic Programming (ICLP), Seattle, WA, USA. Springer, 2006, Lecture Notes in Computer Science (LNCS) 4079, pp. 3-10.
[13] Pientka, B. Eliminating redundancy in higher-order unification: a lightweight approach. In Furbach, U., and Shankar, N., editors, 3rd International Joint Conference on Automated Reasoning, Seattle, WA, USA. SPR, 2006, pp. 362-377.
[14] Pientka, B. Functional programming with higher-order abstract syntax and explicit substitutions. In Programming Languages meets Program Verification (PLPV), Seattle, USA. Elsevier, 2006, Electronic Notes in Theoretical Computer Science (ENTCS), pp. 87-102.
[15] Pientka, B., and Momigliano, A., editors. Proceeding of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Seattle, WA, USA, August 2006, Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier.

Last Update:   2013/08/05 08:24:06.688 GMT-4