Structured Incremental Proof Planning. - Stefan Gerberding; Brigitte Pientka (KI, 1997)

Instantiation of Existentially Quantified Variables in Inductive Specification Proofs. - Brigitte Pientka; Christoph Kreitz (AISC, 1998)

Automating Inductive Specification Proofs. - Brigitte Pientka; Christoph Kreitz (Fundam. Informaticae, 1999)

Matrix-based Constructive Theorem Proving. - Christoph Kreitz; Jens Otten; Stephan Schmitt; Brigitte Pientka (Intellectics and Computational Logic, 2000)

Matrix-Based Inductive Theorem Proving. - Christoph Kreitz; Brigitte Pientka (TABLEAUX, 2000)

Termination and Reduction Checking for Higher-Order Logic Programs. - Brigitte Pientka (IJCAR, 2001)

Connection-Driven Inductive Theorem Proving. - Christoph Kreitz; Brigitte Pientka (Stud Logica, 2001)

A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming. - Brigitte Pientka (ICLP, 2002)

Memoization-Based Proof Search in LF - an Experimental Evaluation of a Prototype. - Brigitte Pientka (LFM, 2002)

Optimizing Higher-Order Pattern Unification. - Brigitte Pientka; Frank Pfenning (CADE, 2003)

A modal foundation for meta-variables. - Aleksandar Nanevski; Brigitte Pientka; Frank Pfenning (MERLIN, 2003)

Higher-Order Substitution Tree Indexing. - Brigitte Pientka (ICLP, 2003)

Tabling for Higher-Order Logic Programming. - Brigitte Pientka (CADE, 2005)

Small Proof Witnesses for LF. - Susmit Sarkar; Brigitte Pientka; Karl Crary (ICLP, 2005)

Verifying Termination and Reduction Properties about Higher-Order Logic Programs. - Brigitte Pientka (J. Autom. Reason., 2005)

Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. - Brigitte Pientka (IJCAR, 2006)

Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks. - Brigitte Pientka (ICLP, 2006)

Preface. - Alberto Momigliano; Brigitte Pientka (LFMTP@FLoC, 2006)

Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions. - Brigitte Pientka (PLPV@IJCAR, 2006)

Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. - Samuli Heilala; Brigitte Pientka (CADE, 2007)

Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. - Brigitte Pientka (TPHOLs, 2007)

Focusing the Inverse Method for LF: A Preliminary Report. - Brigitte Pientka; Xi Li; Florent Pompigne (LFMTP@CADE, 2007)

Preface. - Brigitte Pientka; Carsten Schürmann (LFMTP@CADE, 2007)

A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. - Brigitte Pientka (POPL, 2008)

Programming with proofs and explicit contexts. - Brigitte Pientka; Jana Dunfield (PPDP, 2008)

Case Analysis of Higher-Order Data. - Jana Dunfield; Brigitte Pientka (LFMTP@LICS, 2008)

Contextual modal type theory. - Aleksandar Nanevski; Frank Pfenning; Brigitte Pientka (ACM Trans. Comput. Log., 2008)

Higher-order term indexing using substitution trees. - Brigitte Pientka (ACM Trans. Comput. Log., 2009)

Programming Inductive Proofs - A New Approach Based on Contextual Types. - Brigitte Pientka (Verification, Induction, Termination Analysis, 2010)

Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). - Brigitte Pientka; Jana Dunfield (IJCAR, 2010)

Beluga: Programming with Dependent Types, Contextual Data, and Contexts. - Brigitte Pientka (FLOPS, 2010)

Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. - Amy P. Felty; Brigitte Pientka (ITP, 2010)

Explicit Substitutions for Contextual Type Theory - Andreas Abel 001; Brigitte Pientka (LFMTP, 2010)

Higher-Order Dynamic Pattern Unification for Dependent Types and Records. - Andreas Abel 001; Brigitte Pientka (TLCA, 2011)

Multi-level Contextual Type Theory - Mathieu Boespflug; Brigitte Pientka (LFMTP, 2011)

Intuitionistic Modal Logic and Applications (IMLA 2008). - Valeria de Paiva; Brigitte Pientka (Inf. Comput., 2011)

Preface: Special Issue of Selected Extended Papers of CADE-22. - Renate A. Schmidt; Brigitte Pientka (J. Autom. Reason., 2011)

Programming with binders and indexed data-types. - Andrew Cave; Brigitte Pientka (POPL, 2012)

Wellfounded recursion with copatterns: a unified approach to termination and productivity. - Andreas Abel 001; Brigitte Pientka (ICFP, 2013)

First-class substitutions in contextual type theory. - Andrew Cave; Brigitte Pientka (LFMTP, 2013)

Compiling contextual objects: bringing higher-order abstract syntax to programmers. - Francisco Ferreira 001; Stefan Monnier; Brigitte Pientka (PLPV, 2013)

Copatterns: programming infinite structures by observations. - Andreas Abel 001; Brigitte Pientka; David Thibodeau 001; Anton Setzer (POPL, 2013)

An insider's look at LF type reconstruction: everything you (n)ever wanted to know. - Brigitte Pientka (J. Funct. Program., 2013)

Fair reactive programming. - Andrew Cave; Francisco Ferreira 001; Prakash Panangaden; Brigitte Pientka (POPL, 2014)

Bidirectional Elaboration of Dependently Typed Programs. - Francisco Ferreira 001; Brigitte Pientka (PPDP, 2014)

Unnesting of Copatterns. - Anton Setzer; Andreas Abel 001; Brigitte Pientka; David Thibodeau 001 (RTA-TLCA, 2014)

Inductive Beluga: Programming Proofs. - Brigitte Pientka; Andrew Cave (CADE, 2015)

Mechanizing Meta-Theory in Beluga (Invited Talk). - Brigitte Pientka (WPTE@RDP, 2015)

Well-Founded Recursion over Contextual Objects. - Brigitte Pientka; Andreas Abel 001 (TLCA, 2015)

A Case Study on Logical Relations using Contextual Types. - Andrew Cave; Brigitte Pientka (LFMTP, 2015)

The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks. - Amy P. Felty; Alberto Momigliano; Brigitte Pientka (CoRR, 2015)

An Open Challenge Problem Repository for Systems Supporting Binders. - Amy P. Felty; Alberto Momigliano; Brigitte Pientka (LFMTP, 2015)

The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - A Survey. - Amy P. Felty; Alberto Momigliano; Brigitte Pientka (J. Autom. Reason., 2015)

Programming type-safe transformations using higher-order abstract syntax. - Olivier Savary Bélanger; Stefan Monnier; Brigitte Pientka (J. Formaliz. Reason., 2015)

Indexed codata types. - David Thibodeau 001; Andrew Cave; Brigitte Pientka (ICFP, 2016)

Mechanizing Proofs about Mendler-style Recursion. - Rohan Jacob-Rao; Andrew Cave; Brigitte Pientka (LFMTP, 2016)

Universality of Proofs (Dagstuhl Seminar 16421). - Gilles Dowek; Catherine Dubois; Brigitte Pientka; Florian Rabe 001 (Dagstuhl Reports, 2016)

Well-founded recursion with copatterns and sized types. - Andreas Abel 001; Brigitte Pientka (J. Funct. Program., 2016)

Programs Using Syntax with First-Class Binders. - Francisco Ferreira 001; Brigitte Pientka (ESOP, 2017)

LINCX: A Linear Logical Framework with First-Class Contexts. - Aïna Linn Georges; Agata Murawska; Shawn Otis; Brigitte Pientka (ESOP, 2017)

Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. - Jonas Kaiser; Brigitte Pientka; Gert Smolka (FSCD, 2017)

POPLMark reloaded: mechanizing logical relations proofs (invited talk). - Brigitte Pientka (CPP, 2018)

Index-Stratified Types. - Rohan Jacob-Rao; Brigitte Pientka; David Thibodeau 001 (FSCD, 2018)

Index-Stratified Types (Extended Version). - Rohan Jacob-Rao; Brigitte Pientka; David Thibodeau 001 (CoRR, 2018)

Mechanizing proofs with logical relations - Kripke-style. - Andrew Cave; Brigitte Pientka (Math. Struct. Comput. Sci., 2018)

Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. - Amy P. Felty; Alberto Momigliano; Brigitte Pientka (Math. Struct. Comput. Sci., 2018)

A Type Theory for Defining Logics and Proofs. - Brigitte Pientka; David Thibodeau 001; Andreas Abel 001; Francisco Ferreira 001; Rébecca Zucchini (LICS, 2019)

Cocon: Computation in Contextual Type Theory. - Brigitte Pientka; Andreas Abel 001; Francisco Ferreira 001; David Thibodeau 001; Rébecca Zucchini (CoRR, 2019)

POPLMark reloaded: Mechanizing proofs by logical relations. - Andreas Abel 001; Guillaume Allais; Aliya Hameer; Brigitte Pientka; Alberto Momigliano; Steven Schäfer; Kathrin Stark (J. Funct. Program., 2019)

A case study in programming coinductive proofs: Howe's method. - Alberto Momigliano; Brigitte Pientka; David Thibodeau 001 (Math. Struct. Comput. Sci., 2019)

Teaching the art of functional programming using automated grading (experience report). - Aliya Hameer; Brigitte Pientka (Proc. ACM Program. Lang., 2019)

Semantical Analysis of Contextual Types. - Brigitte Pientka; Ulrich Schöpp (FoSSaCS, 2020)

A Modal Analysis of Metaprogramming, Revisited (Invited Talk). - Brigitte Pientka (FSCD, 2020)

Contextual Types, Explained: Invited Tutorial. - Brigitte Pientka (LICS, 2020)

Harpoon: Mechanizing Metatheory Interactively - (System Description). - Jacob Errington; Junyoung Jang 001; Brigitte Pientka (CADE, 2021)

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 (SIGCSE, 2021)

Moebius: Metaprogramming using Contextual Types - The stage where System F can pattern match on itself (Long Version). - Junyoung Jang 001; Samuel Gélineau; Stefan Monnier; Brigitte Pientka (CoRR, 2021)

Novice Type Error Diagnosis with Natural Language Models. - Chuqin Geng; Haolin Ye; Yixuan Li; Tianyu Han; Brigitte Pientka; Xujie Si (APLAS, 2022)

An Investigation of Kripke-style Modal Type Theories. - Jason Z. S. Hu; Brigitte Pientka (CoRR, 2022)

A Categorical Normalization Proof for the Modal Lambda-Calculus. - Jason Z. S. Hu; Brigitte Pientka (MFPS, 2022)

Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself. - Junyoung Jang 001; Samuel Gélineau; Stefan Monnier; Brigitte Pientka (Proc. ACM Program. Lang., 2022)

A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types. - Jason Z. S. Hu; Brigitte Pientka; Ulrich Schöpp (ACM Trans. Comput. Log., 2022)

Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students. - Chuqin Geng; Wenwen Xu; Yingjie Xu; Brigitte Pientka; Xujie Si (SIGCSE (1), 2023)

Can ChatGPT Pass An Introductory Level Functional Language Programming Course? - Chuqin Geng; Yihan Zhang; Brigitte Pientka; Xujie Si (CoRR, 2023)

Layered Modal Type Theories. - Jason Z. S. Hu; Brigitte Pientka (CoRR, 2023)

Semi-Automation of Meta-Theoretic Proofs in Beluga. - Johanna Schwartzentruber; Brigitte Pientka (LFMTP@FSCD, 2023)

Contextual Refinement Types. - Antoine Gaulin; Brigitte Pientka (LFMTP@FSCD, 2023)

Normalization by evaluation for modal dependent type theory. - Jason Z. S. Hu; Junyoung Jang 001; Brigitte Pientka (J. Funct. Program., 2023)

Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity. - Chuta Sano; Ryan Kavanagh; Brigitte Pientka (Proc. ACM Program. Lang., 2023)

Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis. - Jason Z. S. Hu; Brigitte Pientka (ESOP (1), 2024)

Modernizing SMT-Based Type Error Localization. - Max Kopinsky; Brigitte Pientka; Xujie Si (FMCAD, 2024)

Adjoint Natural Deduction. - Junyoung Jang 001; Sophia Roshal; Frank Pfenning; Brigitte Pientka (FSCD, 2024)

Adjoint Natural Deduction (Extended Version). - Junyoung Jang 001; Sophia Roshal; Frank Pfenning; Brigitte Pientka (CoRR, 2024)

SAT-DIFF: A Tree Diffing Framework Using SAT Solving. - Chuqin Geng; Haolin Ye; Yihan Zhang; Brigitte Pientka; Xujie Si (CoRR, 2024)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming. - Jason Z. S. Hu; Brigitte Pientka (CoRR, 2024)

Polymorphic Metaprogramming with Memory Management - An Adjoint Analysis of Metaprogramming. - Junyoung Jang 001; Brigitte Pientka (CoRR, 2024)

Message-Observing Sessions. - Ryan Kavanagh; Brigitte Pientka (Proc. ACM Program. Lang., 2024)

A Layered Approach to Intensional Analysis in Type Theory. - Jason Z. S. Hu; Brigitte Pientka (ACM Trans. Program. Lang. Syst., 2024)

Split Decisions: Explicit Contexts for Substructural Languages. - Daniel Zackon; Chuta Sano; Alberto Momigliano; Brigitte Pientka (CPP, 2025)

A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract). - Brigitte Pientka (PEPM, 2025)

A Dependent Type Theory for Meta-programming with Intensional Analysis. - Jason Z. S. Hu; Brigitte Pientka (Proc. ACM Program. Lang., 2025)