Brigitte Pientka

124 papers A* 6A 14B 20C 4Misc 3Journal 47Unranked 26

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	A Logical Foundation for Type-Safe Cross-Language Interoperability (Keynote). Programming Brigitte Pientka
2026	J	`jnl`	Evaluating LLMs in the Context of a Functional Programming Course: A Comprehensive Study. CoRR Yihan Zhang, Brigitte Pientka, Xujie Si
2026	J	`jnl`	Evaluating LLMs in the Context of a Functional Programming Course: A Comprehensive Study. Art Sci. Eng. Program. Yihan Zhang, Brigitte Pientka, Xujie Si
2025	J	`jnl`	A Dependent Type Theory for Meta-programming with Intensional Analysis. Proc. ACM Program. Lang. Jason Z. S. Hu, Brigitte Pientka
2025	C	`conf`	A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract). PEPM Brigitte Pientka
2025	J	`jnl`	Deconstructed Proto-Quipper: A Rational Reconstruction. CoRR Ryan Kavanagh, Chuta Sano, Brigitte Pientka
2025	J	`jnl`	Fusing Session-Typed Concurrent Programming into Functional Programming. Proc. ACM Program. Lang. Chuta Sano, Deepak Garg, Ryan Kavanagh, Brigitte Pientka, Bernardo Toninho
2025	J	`jnl`	McTT: A Verified Kernel for a Proof Assistant. Proc. ACM Program. Lang. Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, Brigitte Pientka
2025	B	`conf`	Split Decisions: Explicit Contexts for Substructural Languages. CPP Daniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka
2024	J	`jnl`	A Layered Approach to Intensional Analysis in Type Theory. ACM Trans. Program. Lang. Syst. Jason Z. S. Hu, Brigitte Pientka
2024	J	`jnl`	Adjoint Natural Deduction (Extended Version). CoRR Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka
2024	B	`conf`	Adjoint Natural Deduction. FSCD Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka
2024	J	`jnl`	DeLaM: A Dependent Layered Modal Type Theory for Meta-programming. CoRR Jason Z. S. Hu, Brigitte Pientka
2024	—	`conf`	Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis. ESOP (1) Jason Z. S. Hu, Brigitte Pientka
2024	J	`jnl`	Message-Observing Sessions. CoRR Ryan Kavanagh, Brigitte Pientka
2024	J	`jnl`	Message-Observing Sessions. Proc. ACM Program. Lang. Ryan Kavanagh, Brigitte Pientka
2024	B	`conf`	Modernizing SMT-Based Type Error Localization. FMCAD Max Kopinsky, Brigitte Pientka, Xujie Si
2024	J	`jnl`	Modernizing SMT-Based Type Error Localization. CoRR Max Kopinsky, Brigitte Pientka, Xujie Si
2024	J	`jnl`	Polymorphic Metaprogramming with Memory Management - An Adjoint Analysis of Metaprogramming. CoRR Junyoung Jang, Brigitte Pientka
2024	B	`ed.`	Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024 CPP Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy
2024	J	`jnl`	SAT-DIFF: A Tree Diffing Framework Using SAT Solving. CoRR Chuqin Geng, Haolin Ye, Yihan Zhang, Brigitte Pientka, Xujie Si
2023	A	`ed.`	Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings CADE Brigitte Pientka, Cesare Tinelli
2023	J	`jnl`	Can ChatGPT Pass An Introductory Level Functional Language Programming Course? CoRR Chuqin Geng, Yihan Zhang, Brigitte Pientka, Xujie Si
2023	—	`conf`	Contextual Refinement Types. LFMTP@FSCD Antoine Gaulin, Brigitte Pientka
2023	—	`conf`	Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students. SIGCSE (1) Chuqin Geng, Wenwen Xu, Yingjie Xu, Brigitte Pientka, Xujie Si
2023	J	`jnl`	Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students. CoRR Chuqin Geng, Wenwen Xu, Yingjie Xu, Brigitte Pientka, Xujie Si
2023	J	`jnl`	Layered Modal Type Theories. CoRR Jason Z. S. Hu, Brigitte Pientka
2023	J	`jnl`	Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity. CoRR Chuta Sano, Ryan Kavanagh, Brigitte Pientka
2023	J	`jnl`	Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity. Proc. ACM Program. Lang. Chuta Sano, Ryan Kavanagh, Brigitte Pientka
2023	J	`jnl`	Normalization by evaluation for modal dependent type theory. J. Funct. Program. Jason Z. S. Hu, Junyoung Jang, Brigitte Pientka
2023	B	`ed.`	Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023 CPP Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic
2023	—	`conf`	Semi-Automation of Meta-Theoretic Proofs in Beluga. LFMTP@FSCD Johanna Schwartzentruber, Brigitte Pientka
2022	B	`conf`	A Categorical Normalization Proof for the Modal Lambda-Calculus. MFPS Jason Z. S. Hu, Brigitte Pientka
2022	J	`jnl`	A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types. ACM Trans. Comput. Log. Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp
2022	J	`jnl`	A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types. CoRR Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp
2022	J	`jnl`	An Investigation of Kripke-style Modal Type Theories. CoRR Jason Z. S. Hu, Brigitte Pientka
2022	J	`jnl`	Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself. Proc. ACM Program. Lang. Junyoung Jang, Samuel Gélineau, Stefan Monnier, Brigitte Pientka
2022	B	`conf`	Novice Type Error Diagnosis with Natural Language Models. APLAS Chuqin Geng, Haolin Ye, Yixuan Li, Tianyu Han, Brigitte Pientka, Xujie Si
2022	J	`jnl`	Novice Type Error Diagnosis with Natural Language Models. CoRR Chuqin Geng, Haolin Ye, Yixuan Li, Tianyu Han, Brigitte Pientka, Xujie Si
2021	A	`conf`	Data Collection for the Learn-OCaml Programming Platform: Modelling How Students Develop Typed Functional Programs. SIGCSE Alana Ceci, Hanneli C. A. Tavante, Brigitte Pientka, Xujie Si
2021	A	`conf`	Harpoon: Mechanizing Metatheory Interactively - (System Description). CADE Jacob Errington, Junyoung Jang, Brigitte Pientka
2021	J	`jnl`	Moebius: Metaprogramming using Contextual Types - The stage where System F can pattern match on itself (Long Version). CoRR Junyoung Jang, Samuel Gélineau, Stefan Monnier, Brigitte Pientka
2020	B	`conf`	A Modal Analysis of Metaprogramming, Revisited (Invited Talk). FSCD Brigitte Pientka
2020	A*	`conf`	Contextual Types, Explained: Invited Tutorial. LICS Brigitte Pientka
2020	B	`conf`	Semantical Analysis of Contextual Types. FoSSaCS Brigitte Pientka, Ulrich Schöpp
2019	A*	`conf`	A Type Theory for Defining Logics and Proofs. LICS Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini
2019	J	`jnl`	A Type Theory for Defining Logics and Proofs. CoRR Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini
2019	J	`jnl`	A case study in programming coinductive proofs: Howe's method. Math. Struct. Comput. Sci. Alberto Momigliano, Brigitte Pientka, David Thibodeau
2019	J	`jnl`	Cocon: Computation in Contextual Type Theory. CoRR Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rébecca Zucchini
2019	J	`jnl`	POPLMark reloaded: Mechanizing proofs by logical relations. J. Funct. Program. Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark
2019	J	`jnl`	Teaching the art of functional programming using automated grading (experience report). Proc. ACM Program. Lang. Aliya Hameer, Brigitte Pientka
2018	J	`jnl`	Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Math. Struct. Comput. Sci. Amy P. Felty, Alberto Momigliano, Brigitte Pientka
2018	J	`jnl`	Index-Stratified Types (Extended Version). CoRR Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau
2018	B	`conf`	Index-Stratified Types. FSCD Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau
2018	J	`jnl`	Mechanizing proofs with logical relations - Kripke-style. Math. Struct. Comput. Sci. Andrew Cave, Brigitte Pientka
2018	B	`conf`	POPLMark reloaded: mechanizing logical relations proofs (invited talk). CPP Brigitte Pientka
2017	A	`conf`	LINCX: A Linear Logical Framework with First-Class Contexts. ESOP Aïna Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka
2017	C	`ed.`	Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017 PPDP Wim Vanhoof, Brigitte Pientka
2017	A	`conf`	Programs Using Syntax with First-Class Binders. ESOP Francisco Ferreira, Brigitte Pientka
2017	B	`conf`	Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. FSCD Jonas Kaiser, Brigitte Pientka, Gert Smolka
2016	B	`ed.`	1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, Porto, Portugal, June 22-26, 2016 FSCD Delia Kesner, Brigitte Pientka
2016	A	`conf`	Indexed codata types. ICFP David Thibodeau, Andrew Cave, Brigitte Pientka
2016	—	`conf`	Mechanizing Proofs about Mendler-style Recursion. LFMTP Rohan Jacob-Rao, Andrew Cave, Brigitte Pientka
2016	J	`jnl`	Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe
2016	J	`jnl`	Well-founded recursion with copatterns and sized types. J. Funct. Program. Andreas Abel, Brigitte Pientka
2015	—	`conf`	A Case Study on Logical Relations using Contextual Types. LFMTP Andrew Cave, Brigitte Pientka
2015	—	`conf`	An Open Challenge Problem Repository for Systems Supporting Binders. LFMTP Amy P. Felty, Alberto Momigliano, Brigitte Pientka
2015	A	`conf`	Inductive Beluga: Programming Proofs. CADE Brigitte Pientka, Andrew Cave
2015	—	`conf`	Mechanizing Meta-Theory in Beluga (Invited Talk). WPTE@RDP Brigitte Pientka
2015	J	`jnl`	Programming type-safe transformations using higher-order abstract syntax. J. Formaliz. Reason. Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka
2015	J	`jnl`	The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - A Survey. J. Autom. Reason. Amy P. Felty, Alberto Momigliano, Brigitte Pientka
2015	J	`jnl`	The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks. CoRR Amy P. Felty, Alberto Momigliano, Brigitte Pientka
2015	—	`conf`	Well-Founded Recursion over Contextual Objects. TLCA Brigitte Pientka, Andreas Abel
2014	C	`conf`	Bidirectional Elaboration of Dependently Typed Programs. PPDP Francisco Ferreira, Brigitte Pientka
2014	A*	`conf`	Fair reactive programming. POPL Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka
2014	—	`ed.`	Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014 LFMTP Amy P. Felty, Brigitte Pientka
2014	—	`conf`	Unnesting of Copatterns. RTA-TLCA Anton Setzer, Andreas Abel, Brigitte Pientka, David Thibodeau
2013	J	`jnl`	An insider's look at LF type reconstruction: everything you (n)ever wanted to know. J. Funct. Program. Brigitte Pientka
2013	—	`conf`	Compiling contextual objects: bringing higher-order abstract syntax to programmers. PLPV Francisco Ferreira, Stefan Monnier, Brigitte Pientka
2013	A*	`conf`	Copatterns: programming infinite structures by observations. POPL Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer
2013	—	`conf`	First-class substitutions in contextual type theory. LFMTP Andrew Cave, Brigitte Pientka
2013	—	`ed.`	Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013 LFMTP Alberto Momigliano, Brigitte Pientka, Randy Pollack
2013	B	`conf`	Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. CPP Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka
2013	A	`conf`	Wellfounded recursion with copatterns: a unified approach to termination and productivity. ICFP Andreas Abel, Brigitte Pientka
2012	A*	`conf`	Programming with binders and indexed data-types. POPL Andrew Cave, Brigitte Pientka
2011	—	`conf`	Higher-Order Dynamic Pattern Unification for Dependent Types and Records. TLCA Andreas Abel, Brigitte Pientka
2011	J	`jnl`	Intuitionistic Modal Logic and Applications (IMLA 2008). Inf. Comput. Valeria de Paiva, Brigitte Pientka
2011	—	`conf`	Multi-level Contextual Type Theory LFMTP Mathieu Boespflug, Brigitte Pientka
2011	J	`jnl`	Preface: Special Issue of Selected Extended Papers of CADE-22. J. Autom. Reason. Renate A. Schmidt, Brigitte Pientka
2010	A	`conf`	Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). IJCAR Brigitte Pientka, Jana Dunfield
2010	Misc	`conf`	Beluga: Programming with Dependent Types, Contextual Data, and Contexts. FLOPS Brigitte Pientka
2010	—	`conf`	Explicit Substitutions for Contextual Type Theory LFMTP Andreas Abel, Brigitte Pientka
2010	—	`conf`	Programming Inductive Proofs - A New Approach Based on Contextual Types. Verification, Induction, Termination Analysis Brigitte Pientka
2010	B	`conf`	Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. ITP Amy P. Felty, Brigitte Pientka
2009	J	`jnl`	Higher-order term indexing using substitution trees. ACM Trans. Comput. Log. Brigitte Pientka
2008	A*	`conf`	A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. POPL Brigitte Pientka
2008	—	`conf`	Case Analysis of Higher-Order Data. LFMTP@LICS Jana Dunfield, Brigitte Pientka
2008	J	`jnl`	Contextual modal type theory. ACM Trans. Comput. Log. Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka
2008	—	`ed.`	Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007 LFMTP@CADE Brigitte Pientka, Carsten Schürmann
2008	C	`conf`	Programming with proofs and explicit contexts. PPDP Brigitte Pientka, Jana Dunfield
2007	A	`conf`	Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. CADE Samuli Heilala, Brigitte Pientka
2007	—	`conf`	Focusing the Inverse Method for LF: A Preliminary Report. LFMTP@CADE Brigitte Pientka, Xi Li, Florent Pompigne
2007	—	`conf`	Preface. LFMTP@CADE Brigitte Pientka, Carsten Schürmann
2007	—	`ed.`	Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006 LFMTP@FLoC Alberto Momigliano, Brigitte Pientka
2007	—	`conf`	Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. TPHOLs Brigitte Pientka
2006	A	`conf`	Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. IJCAR Brigitte Pientka
2006	—	`conf`	Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions. PLPV@IJCAR Brigitte Pientka
2006	B	`conf`	Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks. ICLP Brigitte Pientka
2006	—	`conf`	Preface. LFMTP@FLoC Alberto Momigliano, Brigitte Pientka
2005	B	`conf`	Small Proof Witnesses for LF. ICLP Susmit Sarkar, Brigitte Pientka, Karl Crary
2005	A	`conf`	Tabling for Higher-Order Logic Programming. CADE Brigitte Pientka
2005	J	`jnl`	Verifying Termination and Reduction Properties about Higher-Order Logic Programs. J. Autom. Reason. Brigitte Pientka
2003	—	`conf`	A modal foundation for meta-variables. MERLIN Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning
2003	B	`conf`	Higher-Order Substitution Tree Indexing. ICLP Brigitte Pientka
2003	A	`conf`	Optimizing Higher-Order Pattern Unification. CADE Brigitte Pientka, Frank Pfenning
2002	B	`conf`	A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming. ICLP Brigitte Pientka
2002	—	`conf`	Memoization-Based Proof Search in LF - an Experimental Evaluation of a Prototype. LFM Brigitte Pientka
2001	J	`jnl`	Connection-Driven Inductive Theorem Proving. Stud Logica Christoph Kreitz, Brigitte Pientka
2001	A	`conf`	Termination and Reduction Checking for Higher-Order Logic Programs. IJCAR Brigitte Pientka
2000	B	`conf`	Matrix-Based Inductive Theorem Proving. TABLEAUX Christoph Kreitz, Brigitte Pientka
2000	—	`conf`	Matrix-based Constructive Theorem Proving. Intellectics and Computational Logic Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka
1999	J	`jnl`	Automating Inductive Specification Proofs. Fundam. Informaticae Brigitte Pientka, Christoph Kreitz
1998	Misc	`conf`	Instantiation of Existentially Quantified Variables in Inductive Specification Proofs. AISC Brigitte Pientka, Christoph Kreitz
1997	Misc	`conf`	Structured Incremental Proof Planning. KI Stefan Gerberding, Brigitte Pientka