Publications

Journals

• Higher-order term indexing using substitution tree, Brigitte Pientka, ACM Transactions on Computational Logic, vol 11, issue 1 (October 2009).
• Contextual modal type theory, Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka, (60 pages), ACM Transactions on Computational Logic, vol 9, issue 3, 2008.
• Verifying termination and reduction properties about higher-order logic programs Brigitte Pientka, Journal of Automated Reasoning (JAR), vol 34, issue 2, pages 179 - 207, 2005.
• Connection-Driven Induction Theorem Proving, Christoph Kreitz and Brigitte Pientka.
  Studia Logica, Kluwer, vol 69, issue 2, pages 293 - 326, 2001
• Automating inductive Specification Proofs in Nuprl, Brigitte Pientka, Christoph Kreitz,Fundamenta Informaticae, vol 39, issue 1-2, pages 189 - 209, 2001.

Conferences

• 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), pages 163 - 173, ACM Press, 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.
• Proof Pearl:The power of higher-order encodings in the logical framework LF , Brigitte Pientka, 20th International Conference on Theorem Proving in Higher-order Logics(TPHOLs'07), Kaiserslautern, Germany, pages 246 - 261, LNCS 4732, Springer, 2007, code.
• Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4 , Samuli Heilala and Brigitte Pientka, 21st International Conference of Automated Deduction (CADE'07), Bremen, Germany, pages 116 - 131, LNCS 4603, Springer, 2007.
• Overcoming perfomrance barriers: efficient verification techniques for logical frameworks, Brigitte Pientka, 22nd International Conference on Logic Programming (ICLP'06), Seattle, USA, pages 3 - 10, LNCS 4079, Springer, 2006 (invited tutorial, slides).
• Eliminating redundancy in higher-order unification: a lightweight approach, Brigitte Pientka, 3rd International Joint Conference on Automated Reasoning (IJCAR'06), Seattle, USA, pages 362 - 377, LNAI 4130, Springer, 2006.
• Small proof witnesses for LF, Susmit Sarkar, Brigitte Pientka, Karl Crary, 21th International Conference on Logic Programming (ICLP'05), Barcelona, Spain, pages 387 - 401, LNCS 3668, Springer, 2005.
• Tabling for higher-order logic programming, Brigitte Pientka, 20th International Conference on Automated Deduction (CADE'05), Talinn, Estonia, pages 54 - 69, LNCS 3632, Springer, 2005.
• Higher-order substitution tree indexing, Brigitte Pientka,
  19th International Conference on Logic Programming (ICLP'03), (ICLP), Mumbai, India, pages 377 - 391, LNCS 2916, Springer, 2003.
  (Best student paper award)
• Optimizing higher-order pattern unification, Brigitte Pientka, Frank Pfenning.
  19th International Conference on Automated Deduction (CADE'03), Miami, Florida, USA, pages 473 - 487, LNAI 2741, Springer, 2003.
• A proof-theoretic foundation for tabled higher-order logic programming,(slides) Brigitte Pientka.
  18th International Conference on Logic Programming (ICLP'02) , Copenhagen, Denmark, pages 271 - 286, LNCS 2401, Springer, 2002.
• Termination and Reduction Checking for Higher-Order Logic Programs, Brigitte Pientka.
  First International Joint Conference on Automated Reasoning (IJCAR'01), Siena, Italy, pages 401 - 415, LNCS 2083, Springer, 2001, Twelf code
• Matrix-based inductive Theorem Proving, Christoph Kreitz , Brigitte Pientka, International Conference  TABLEAUX-2000, St. Andrews, Scotland, pages 294 - 308, LNAI 1847, Springer, 2000.
• Automatic Instantiation of Meta-Variables in inductive Specification Proofs, Brigitte Pientka, Christoph Kreitz, 4th International Conference on Symbolic Computation and Artificial Intelligence, Plattsburgh, NY, USA, Springer,1998
• Structured Incremental Proof Planning, Stefan Gerberding, Brigitte Pientka, Proceedings of the 21th German Annual Conference on Artificial Intelligence, Freiburg, Germany, Springer, 1997

Workshops

• Case analysis on higher-order data, Joshua Dunfield and Brigitte Pientka, a revised version will appear at International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08), 2008
• Focusing the inverse method for LF: a preliminary report,Brigitte Pientka, David Xi Li, Florent Pompigne, International Workshop on Logical Frameworks and Meta-languages:Theory and Practice, Bremen, Germany, July 2007
• Functional programming with higher-order abstract syntax and explicit substitutions, Brigitte Pientka, Programming Languages meets Program Verification (PLPV), August 21, 2006 (This paper is superseeded by the paper "A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions").
• A modal foundation for meta-variables, Aleksander Nanevski, Brigitte Pientka, Frank Pfenning,
  2nd ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with variable binding (Merlin), September 2003. (This paper is superseeded by the article Contextual modal type theory, which appeared in ACM Transactions on Computational Logic in 2008.)
• Memoization-based proof search in LF: an experimental evaluation of a prototype, (slides)Brigitte Pientka.
  Third International Workshop on Logical Frameworks and Meta-Languages (LFM'02), July 2002, Copenhagen, Denmark, Electronic Notes on Theoretical Computer Science (ENTCS)
• Matrix-based inductive Theorem Proving, Christoph Kreitz , Brigitte Pientka, Workshop on Automating Proofs by Induction (This paper is superseeded by the Tableaux-200 paper.)