Publications

Journals

• Jason Z.S. Hu and Junyoung Jang and Brigitte Pientka. Normalization by evaluation for modal dependent type theory, Journal of Functional Programming (JFP), Oct 2023
• Jason Z.S. Hu and Brigitte Pientka, and Ulrich Schoepp. A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types, ACM Transactions of Computational Logic (TOCL) (doi, July 2022
• Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark: POPLMark Reloaded: Mechanizing Logical Relations Proofs, J. Funct. Program. 29:(e19), 2019
• Alberto Momigliano, Brigitte Pientka, David Thibodeau: A case study in programming coinductive proofs: Howe's method. Math. Struct. Comput. Sci. 29(8): 1309-1343 (2019)
• Andrew Cave and Brigitte Pientka. Mechanizing Proofs with Logical Relations --Kripke-style, Mathematical Structures in Computer Science, accepted and in print June 2018.
• Olivier Savary Belanger, Stefan Monnier, Brigitte Pientka. Programming Type-safe Transformations using Higher-order Abstract Syntax. Journal of Formalized Reasoning. 8(1): 49-91, 2015 (This is the long and revised version of the CPP'13 paper) (pdf + Beluga code)
• Amy Felty, Alberto Momigliano, Brigitte Pientka. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2 - A Survey (including the electronic appendix). Journal of Automated Reasoning, 55(4): 307-372, 2015
• Andreas Abel, Brigitte Pientka. Well-founded Recursion with Copatterns: A Unified Approach to Termination and Productivity, accepted at the Journal of Functional Programming (Nov 2015).
• Olivier Savary Belanger, Stefan Monnier, Brigitte Pientka. Programming Type-safe Transformations using Higher-order Abstract Syntax. Journal of Formalized Reasoning. 8(1): 49-91, 2015 (This is the long and revised version of the CPP'13 paper) (pdf + Beluga code)
• Amy Felty, Alberto Momigliano, Brigitte Pientka. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2 - A Survey (including the electronic appendix), Journal of Automated Reasoning, 55(4): 307-372, 2015
• Brigitte Pientka. An insider's look at LF type reconstruction:Everything you (n)ever wanted to know,Journal of Functional Programming, Jan 2013
• Higher-order term indexing using substitution tree, Brigitte Pientka, ACM Transactions on Computational Logic, 11(1):1-40, 2009.
• Contextual modal type theory, Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka, ACM Transactions on Computational Logic, 9(3):1-60, 2008.
• Verifying termination and reduction properties about higher-order logic programs Brigitte Pientka, Journal of Automated Reasoning, 34(2):179-207, 2005.
• Connection-Driven Induction Theorem Proving, Christoph Kreitz and Brigitte Pientka. Studia Logica, 69(2):293--326, 2001.
• Automating inductive Specification Proofs in Nuprl, Brigitte Pientka, Christoph Kreitz, Fundamenta Informaticae, 39(1--2):189-209, 1999.

Conferences

• Chuta Sano and Ryan Kavanagh and Brigitte Pientka. Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity, OOPSLA'2023, Oct 2023
• Chuqin Geng, Wenwen Xu, Yingjie Xu, Brigitte Pientka, Xujie Si. Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students. 54th ACM Technical Symposium on Computer Science Education (SIGCSE - Vol 1) 2023
• Junyoung Jang, Samuel Gélineau, Stefan Monnier, Brigitte Pientka, Moebius: Metaprogramming using contextual types-- the stage where system f can pattern match on itself, POPL 2022
• Jacob Errington, Junyoung Jang, Brigitte Pientka, Harpoon: Mechanizing Metatheory Interactively - (System Description), CADE 2021
• Brigitte Pientka, Ulrich Schoepp. Semantical Analysis of Contextual Types, FoSSaCS 2020.
• Aliya Hameer, Brigitte Pientka. Teaching the Art of Functional Programming Using Automated Grading (Experience Report) accepted at ICFP'19
• Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rebecca Zucchini. A Type Theory for Defining Logics and Proofs accepted at LICS'19
• David Thibodeau, Alberto Momigliano, Brigitte Pientka. A Case-Study in Programming Coinductive Proofs: Howe's Method, accepted at MSCS in 2018.
• Rohan Jacob-Rao, Brigitte Pientka, and David Thibodeau. Index-Stratified Types, International Conference on Formal Structures for Computation and Deduction (FSCD'18): 19:1-19:17, LiPICS 2018
• Andrew Cave and Brigitte Pientka. Mechanizing Proofs with Logical Relations --Kripke-style, Mathematical Structures in Computer Science, accepted and in print June 2018.
• Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating System F and Lambda2: A Case Study in Coq, Abella, and Beluga, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD'17); more details, in particular the code for each case study can be found in the online repository.
• Aina Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka. Lincx: A Linear Logical Framework with First-Class Contexts, 26th European Symposium on Programming (ESOP'17), 2017
• Francisco Ferreira, Brigitte Pientka. Programs Using Syntax with First-Class Binders, 26th European Symposium on Programming (ESOP'17), 2017
• Amy Felty, Alberto Momigliano, Brigitte Pientka. Benchmarks for Reasoning with Syntax Trees Containing Binders and Contexts of Assumptions accepted in Mathematical Structures in Computer Science (MSCS), 2017.
• David Thibodeau, Andrew Cave, Brigitte Pientka. Indexed Codata Types (submitted March 2016), International Conference on Functional Programming (ICFP'16)
• Brigitte Pientka and Andrew Cave. Inductive Beluga: Programming Proofs (System Description), 25th International Conference on Automated Deduction (CADE-25), LNCS 9195, pages 272-281, Springer, 2015.
• Brigitte Pientka and Andreas Abel. Structural Recursion over Contextual Objects, (Long version (older draft from Feb 2015))), 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15), pages 273-287, LiPICS, 2015
• Francisco Ferreira, Brigitte Pientka, Bidirectional Elaboration of Dependently Typed Programs, 16th International Symposium on Principles and Practice of Declarative Programming (PPDP'14), pages 161-174, ACM, 2014. (long version including soundness proof)
• Anton Setzer, Andreas Abel, Brigitte Pientka and David Thibodeau. Unnesting of Copatterns, Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA'14), LNCS 8560, pages 31-45, Springer, 2014
• Andrew Cave, Francisco Ferreira, Prakash Panangaden, and Brigitte Pientka. Fair reactive programming, 41th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14), pages 361-372, ACM, 2014. (Long version).
• Olivier Savary-Belanger, Stefan Monnier and Brigitte Pientka. Programming type-safe transformations using higher-order abstract syntax, Beluga code, 3rd International Conference on Certified Programs and Proofs (CPP'13), LNCS 8307, pages 243-258, Springer, 2013.
• Andreas Abel and Brigitte Pientka. Well-founded Recursion with Copatterns:A Unified Approach to Termination and Productivity, 18th ACM SIGPLAN International Conference on FunctionalProgramming (ICFP'13), pages 185-196, ACM, 2014. (long version available ).
• Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer. Copatterns: Programming Infinite Structures by Observations, 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), pages 27-38, ACM, 2013.
• Andrew Cave and Brigitte Pientka. Programming with Binders and Indexed Data-types, 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12), pages 413-424, ACM, 2012.
• Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records, 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11), LNCS 6690, pages 10-26, Springer, 2011. (long version)
• Beluga: programming with dependent types, contextual data, and contexts,Brigitte Pientka, Invited talk at 10th International Symposium on Functional and Logic Programming (FLOPS'10), pages 3-10, LNCS 4079, Springer, 2010.
• Programming inductive proofs: a new approach based on contextual types, Brigitte Pientka, Verification, Induction, and Termination analysis, pages 1 - 16, LNCS 6463, Springer, 2010
• Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison,Amy Felty and Brigitte Pientka, First International Conference on Interactive Theorem Proving (ITP'10) (Electronic Appendix (pdf, mechanized proofs and examples), pages 227-242, LNCS 6172, Springer, 2010
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System description),Brigitte Pientka and Joshua Dunfield, 5th International Joint Conference on Automated Reasoning (JCAR'10), pages 15-21, LNCS 6173, Springer, 2010
• 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

• Antoine Gaulin and Brigitte Pientka. Contextual Refinement Types, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'23), July 2023
• Johanna Schwartzentruber and Brigitte Pientka. Semi-Automation of Meta-Theoretic Proofs in Beluga, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'23), July 2023
• Rohan Jacob-Rao, Andrew Cave and Brigitte Pientka. Mechanizing Proofs about Mendler-Recursion, 11th Workshop Logical Frameworks and Meta-languages (LFMTP'16): Theory and Practice, 2016
• Andrew Cave and Brigitte Pientka. A Case Study on Logical Relations using Contextual Types, 10th Workshop Logical Frameworks and Meta-languages (LFMTP'15): Theory and Practice, pages 3-18, EPTCS, 2015
• Amy Felty, Alberto Momigliano, and Brigitte Pientka. , 10th Workshop on Logical Frameworks and Meta-Languages (LFMTP;15): Theory and Practice, pages 18-33, EPTCS, 2015.
• Andrew Cave and Brigitte Pientka. First-class substitutions in contextual type theory, 8th Workshop on Logical Frameworks and Meta-Languages (LFMTP'13): Theory and Practice, 2013.
• Mathieu Boespflug and Brigitte Pientka. Multi-level Contextual Type Theory, 6th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'11) (long version).
• 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 )
• 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.)

Technical reports

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