| 2025 | CPP | Split Decisions: Explicit Contexts for Substructural Languages. | Daniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka |
| 2025 | PEPM | A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract). | Brigitte Pientka |
| 2024 | ESOP | Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis. | Jason Z. S. Hu, Brigitte Pientka |
| 2024 | FMCAD | Modernizing SMT-Based Type Error Localization. | Max Kopinsky, Brigitte Pientka, Xujie Si |
| 2024 | FSCD | Adjoint Natural Deduction. | Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka |
| 2023 | SIGCSE | Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students. | Chuqin Geng, Wenwen Xu, Yingjie Xu, Brigitte Pientka, Xujie Si |
| 2022 | APLAS | Novice Type Error Diagnosis with Natural Language Models. | Chuqin Geng, Haolin Ye, Yixuan Li, Tianyu Han, Brigitte Pientka, Xujie Si |
| 2021 | CADE | Harpoon: Mechanizing Metatheory Interactively - (System Description). | Jacob Errington, Junyoung Jang, Brigitte Pientka |
| 2021 | SIGCSE | Data Collection for the Learn-OCaml Programming Platform: Modelling How Students Develop Typed Functional Programs. | Alana Ceci, Hanneli C. A. Tavante, Brigitte Pientka, Xujie Si |
| 2020 | FOSSACS | Semantical Analysis of Contextual Types. | Brigitte Pientka, Ulrich Schpp |
| 2020 | FSCD | A Modal Analysis of Metaprogramming, Revisited (Invited Talk). | Brigitte Pientka |
| 2020 | LICS | Contextual Types, Explained: Invited Tutorial. | Brigitte Pientka |
| 2019 | LICS | A Type Theory for Defining Logics and Proofs. | Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rbecca Zucchini |
| 2018 | CPP | POPLMark reloaded: mechanizing logical relations proofs (invited talk). | Brigitte Pientka |
| 2017 | ESOP | Programs Using Syntax with First-Class Binders. | Francisco Ferreira, Brigitte Pientka |
| 2017 | ESOP | LINCX: A Linear Logical Framework with First-Class Contexts. | Ana Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka |
| 2016 | ICFP | Indexed codata types. | David Thibodeau, Andrew Cave, Brigitte Pientka |
| 2015 | CADE | Inductive Beluga: Programming Proofs. | Brigitte Pientka, Andrew Cave |
| 2014 | POPL | Fair reactive programming. | Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka |
| 2014 | PPDP | Bidirectional Elaboration of Dependently Typed Programs. | Francisco Ferreira, Brigitte Pientka |
| 2013 | CPP | Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. | Olivier Savary Blanger, Stefan Monnier, Brigitte Pientka |
| 2013 | ICFP | Wellfounded recursion with copatterns: a unified approach to termination and productivity. | Andreas Abel, Brigitte Pientka |
| 2013 | POPL | Copatterns: programming infinite structures by observations. | Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer |
| 2012 | POPL | Programming with binders and indexed data-types. | Andrew Cave, Brigitte Pientka |
| 2010 | CADE | Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). | Brigitte Pientka, Jana Dunfield |
| 2010 | FLOPS | Beluga: Programming with Dependent Types, Contextual Data, and Contexts. | Brigitte Pientka |
| 2010 | ITP | Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. | Amy P. Felty, Brigitte Pientka |
| 2008 | POPL | A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. | Brigitte Pientka |
| 2008 | PPDP | Programming with proofs and explicit contexts. | Brigitte Pientka, Jana Dunfield |
| 2007 | CADE | Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. | Samuli Heilala, Brigitte Pientka |
| 2006 | CADE | Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. | Brigitte Pientka |
| 2006 | ICLP | Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks. | Brigitte Pientka |
| 2005 | CADE | Tabling for Higher-Order Logic Programming. | Brigitte Pientka |
| 2005 | ICLP | Small Proof Witnesses for LF. | Susmit Sarkar, Brigitte Pientka, Karl Crary |
| 2003 | CADE | Optimizing Higher-Order Pattern Unification. | Brigitte Pientka, Frank Pfenning |
| 2003 | ICFP | A modal foundation for meta-variables. | Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning |
| 2003 | ICLP | Higher-Order Substitution Tree Indexing. | Brigitte Pientka |
| 2002 | ICLP | A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming. | Brigitte Pientka |
| 2001 | CADE | Termination and Reduction Checking for Higher-Order Logic Programs. | Brigitte Pientka |
| 2000 | TABLEAUX | Matrix-Based Inductive Theorem Proving. | Christoph Kreitz, Brigitte Pientka |
| 1998 | AISC | Instantiation of Existentially Quantified Variables in Inductive Specification Proofs. | Brigitte Pientka, Christoph Kreitz |
| 1997 | KI | Structured Incremental Proof Planning. | Stefan Gerberding, Brigitte Pientka |