Brigitte Pientka

ORCID

Publication Activity (10 Years)

Years Active: 1997-2024
Publications (10 Years): 47

Top Venues

CoRR

FSCD

Proc. ACM Program. Lang.

Math. Struct. Comput. Sci.

Publications

Jason Z. S. Hu, Brigitte Pientka
DeLaM: A Dependent Layered Modal Type Theory for Meta-programming. CoRR (2024)
Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka
Adjoint Natural Deduction (Extended Version). CoRR (2024)
Ryan Kavanagh, Brigitte Pientka
Message-Observing Sessions. CoRR (2024)
Chuqin Geng, Haolin Ye, Yihan Zhang, Brigitte Pientka, Xujie Si
SAT-DIFF: A Tree Diffing Framework Using SAT Solving. CoRR (2024)
Jason Z. S. Hu, Brigitte Pientka
Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis. ESOP (1) (2024)
Ryan Kavanagh, Brigitte Pientka
Message-Observing Sessions. Proc. ACM Program. Lang. 8 (OOPSLA1) (2024)
Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka
Adjoint Natural Deduction. FSCD (2024)
Chuqin Geng, Wenwen Xu, Yingjie Xu, Brigitte Pientka, Xujie Si
Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students. SIGCSE (1) (2023)
Jason Z. S. Hu, Junyoung Jang, Brigitte Pientka
Normalization by evaluation for modal dependent type theory. J. Funct. Program. 33 (2023)
Chuqin Geng, Yihan Zhang, Brigitte Pientka, Xujie Si
Can ChatGPT Pass An Introductory Level Functional Language Programming Course? CoRR (2023)
Johanna Schwartzentruber, Brigitte Pientka
Semi-Automation of Meta-Theoretic Proofs in Beluga. CoRR (2023)
Jason Z. S. Hu, Brigitte Pientka
Layered Modal Type Theories. CoRR (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. CoRR (2023)
Chuta Sano, Ryan Kavanagh, Brigitte Pientka
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity. CoRR (2023)
Antoine Gaulin, Brigitte Pientka
Contextual Refinement Types. CoRR (2023)
Chuta Sano, Ryan Kavanagh, Brigitte Pientka
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Junyoung Jang, Samuel Gélineau, Stefan Monnier, Brigitte Pientka
Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself. Proc. ACM Program. Lang. 6 (POPL) (2022)
Jason Z. S. Hu, Brigitte Pientka
An Investigation of Kripke-style Modal Type Theories. CoRR (2022)
Chuqin Geng, Haolin Ye, Yixuan Li, Tianyu Han, Brigitte Pientka, Xujie Si
Novice Type Error Diagnosis with Natural Language Models. CoRR (2022)
Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types. CoRR (2022)
Jason Z. S. Hu, Brigitte Pientka
A Categorical Normalization Proof for the Modal Lambda-Calculus. CoRR (2022)
Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp
A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types. ACM Trans. Comput. Log. 23 (4) (2022)
Chuqin Geng, Haolin Ye, Yixuan Li, Tianyu Han, Brigitte Pientka, Xujie Si
Novice Type Error Diagnosis with Natural Language Models. APLAS (2022)
Jacob Errington, Junyoung Jang, Brigitte Pientka
Harpoon: Mechanizing Metatheory Interactively - (System Description). CADE (2021)
Junyoung Jang, Samuel Gélineau, Stefan Monnier, Brigitte Pientka
Moebius: Metaprogramming using Contextual Types - The stage where System F can pattern match on itself (Long Version). CoRR (2021)
Alana Ceci, Hanneli C. A. Tavante, Brigitte Pientka, Xujie Si
Data Collection for the Learn-OCaml Programming Platform: Modelling How Students Develop Typed Functional Programs. SIGCSE (2021)
Brigitte Pientka
Contextual Types, Explained: Invited Tutorial. LICS (2020)
Brigitte Pientka
A Modal Analysis of Metaprogramming, Revisited (Invited Talk). FSCD (2020)
Brigitte Pientka, Ulrich Schöpp
Semantical Analysis of Contextual Types. FoSSaCS (2020)
Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rébecca Zucchini
Cocon: Computation in Contextual Type Theory. CoRR (2019)
Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini
A Type Theory for Defining Logics and Proofs. CoRR (2019)
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark
POPLMark reloaded: Mechanizing proofs by logical relations. J. Funct. Program. 29 (2019)
Aliya Hameer, Brigitte Pientka
Teaching the art of functional programming using automated grading (experience report). Proc. ACM Program. Lang. 3 (ICFP) (2019)
Alberto Momigliano, Brigitte Pientka, David Thibodeau
A case study in programming coinductive proofs: Howe's method. Math. Struct. Comput. Sci. 29 (8) (2019)
Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini
A Type Theory for Defining Logics and Proofs. LICS (2019)
Brigitte Pientka
POPLMark reloaded: mechanizing logical relations proofs (invited talk). CPP (2018)
Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau
Index-Stratified Types (Extended Version). CoRR (2018)
Andrew Cave, Brigitte Pientka
Mechanizing proofs with logical relations - Kripke-style. Math. Struct. Comput. Sci. 28 (9) (2018)
Amy P. Felty, Alberto Momigliano, Brigitte Pientka
Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Math. Struct. Comput. Sci. 28 (9) (2018)
Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau
Index-Stratified Types. FSCD (2018)
Jonas Kaiser, Brigitte Pientka, Gert Smolka
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. FSCD (2017)
Aïna Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka
LINCX: A Linear Logical Framework with First-Class Contexts. ESOP (2017)
Francisco Ferreira, Brigitte Pientka
Programs Using Syntax with First-Class Binders. ESOP (2017)
Rohan Jacob-Rao, Andrew Cave, Brigitte Pientka
Mechanizing Proofs about Mendler-style Recursion. LFMTP (2016)
Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe
Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports 6 (10) (2016)
Andreas Abel, Brigitte Pientka
Well-founded recursion with copatterns and sized types. J. Funct. Program. 26 (2016)
David Thibodeau, Andrew Cave, Brigitte Pientka
Indexed codata types. ICFP (2016)
Amy P. Felty, Alberto Momigliano, Brigitte Pientka
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - A Survey. J. Autom. Reason. 55 (4) (2015)
Brigitte Pientka, Andreas Abel
Well-Founded Recursion over Contextual Objects. TLCA (2015)
Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka
Programming type-safe transformations using higher-order abstract syntax. J. Formaliz. Reason. 8 (1) (2015)
Amy P. Felty, Alberto Momigliano, Brigitte Pientka
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks. CoRR (2015)
Brigitte Pientka, Andrew Cave
Inductive Beluga: Programming Proofs. CADE (2015)
Brigitte Pientka
Mechanizing Meta-Theory in Beluga (Invited Talk). WPTE@RTA/TLCA (2015)
Andrew Cave, Brigitte Pientka
A Case Study on Logical Relations using Contextual Types. LFMTP (2015)
Amy P. Felty, Alberto Momigliano, Brigitte Pientka
An Open Challenge Problem Repository for Systems Supporting Binders. LFMTP (2015)
Anton Setzer, Andreas Abel, Brigitte Pientka, David Thibodeau
Unnesting of Copatterns. RTA-TLCA (2014)
Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka
Fair reactive programming. POPL (2014)
Francisco Ferreira, Brigitte Pientka
Bidirectional Elaboration of Dependently Typed Programs. PPDP (2014)
Francisco Ferreira, Stefan Monnier, Brigitte Pientka
Compiling contextual objects: bringing higher-order abstract syntax to programmers. PLPV (2013)
Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka
Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. CPP (2013)
Andrew Cave, Brigitte Pientka
First-class substitutions in contextual type theory. LFMTP (2013)
Brigitte Pientka
An insider's look at LF type reconstruction: everything you (n)ever wanted to know. J. Funct. Program. 23 (1) (2013)
Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer
Copatterns: programming infinite structures by observations. POPL (2013)
Andreas Abel, Brigitte Pientka
Wellfounded recursion with copatterns: a unified approach to termination and productivity. ICFP (2013)
Andrew Cave, Brigitte Pientka
Programming with binders and indexed data-types. POPL (2012)
Mathieu Boespflug, Brigitte Pientka
Multi-level Contextual Type Theory LFMTP (2011)
Andreas Abel, Brigitte Pientka
Higher-Order Dynamic Pattern Unification for Dependent Types and Records. TLCA (2011)
Renate A. Schmidt, Brigitte Pientka
Preface: Special Issue of Selected Extended Papers of CADE-22. J. Autom. Reason. 47 (2) (2011)
Valeria de Paiva, Brigitte Pientka
Intuitionistic Modal Logic and Applications (IMLA 2008). Inf. Comput. 209 (12) (2011)
Brigitte Pientka, Jana Dunfield
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). IJCAR (2010)
Brigitte Pientka
Beluga: Programming with Dependent Types, Contextual Data, and Contexts. FLOPS (2010)
Amy P. Felty, Brigitte Pientka
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. ITP (2010)
Brigitte Pientka
Programming Inductive Proofs - A New Approach Based on Contextual Types. Verification, Induction, Termination Analysis (2010)
Andreas Abel, Brigitte Pientka
Explicit Substitutions for Contextual Type Theory LFMTP (2010)
Brigitte Pientka
Higher-order term indexing using substitution trees. ACM Trans. Comput. Log. 11 (1) (2009)
Jana Dunfield, Brigitte Pientka
Case Analysis of Higher-Order Data. Electron. Notes Theor. Comput. Sci. 228 (2009)
Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka
Contextual modal type theory. ACM Trans. Comput. Log. 9 (3) (2008)
Brigitte Pientka, Xi Li, Florent Pompigne
Focusing the Inverse Method for LF: A Preliminary Report. Electron. Notes Theor. Comput. Sci. 196 (2008)
Brigitte Pientka, Carsten Schürmann
Preface. Electron. Notes Theor. Comput. Sci. 196 (2008)
Brigitte Pientka, Jana Dunfield
Programming with proofs and explicit contexts. PPDP (2008)
Brigitte Pientka
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. POPL (2008)
Brigitte Pientka
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. TPHOLs (2007)
Alberto Momigliano, Brigitte Pientka
Preface. Electron. Notes Theor. Comput. Sci. 174 (5) (2007)
Brigitte Pientka
Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions. Electron. Notes Theor. Comput. Sci. 174 (7) (2007)
Samuli Heilala, Brigitte Pientka
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. CADE (2007)
Brigitte Pientka
Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks. ICLP (2006)
Brigitte Pientka
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. IJCAR (2006)
Susmit Sarkar, Brigitte Pientka, Karl Crary
Small Proof Witnesses for LF. ICLP (2005)
Brigitte Pientka
Tabling for Higher-Order Logic Programming. CADE (2005)
Brigitte Pientka
Verifying Termination and Reduction Properties about Higher-Order Logic Programs. J. Autom. Reason. 34 (2) (2005)
Brigitte Pientka
Higher-Order Substitution Tree Indexing. ICLP (2003)
Brigitte Pientka, Frank Pfenning
Optimizing Higher-Order Pattern Unification. CADE (2003)
Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning
A modal foundation for meta-variables. MERLIN (2003)
Brigitte Pientka
Memoization-Based Proof Search in LF - an Experimental Evaluation of a Prototype. Electron. Notes Theor. Comput. Sci. 70 (2) (2002)
Brigitte Pientka
A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming. ICLP (2002)
Christoph Kreitz, Brigitte Pientka
Connection-Driven Inductive Theorem Proving. Stud Logica 69 (2) (2001)
Brigitte Pientka
Termination and Reduction Checking for Higher-Order Logic Programs. IJCAR (2001)
Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka
Matrix-based Constructive Theorem Proving. Intellectics and Computational Logic (2000)
Christoph Kreitz, Brigitte Pientka
Matrix-Based Inductive Theorem Proving. TABLEAUX (2000)
Brigitte Pientka, Christoph Kreitz
Automating Inductive Specification Proofs. Fundam. Informaticae 39 (1-2) (1999)

Brigitte Pientka.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Brigitte Pientka