Остановите войну!
for scientists:
default search action
Brigitte Pientka
- > Home > Persons > Brigitte Pientka
Publications
- 2024
- [c63]Jason Z. S. Hu, Brigitte Pientka:
Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis. ESOP (1) 2024: 52-82 - [e9]Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy:
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024. ACM 2024 [contents] - [i15]Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka:
Adjoint Natural Deduction (Extended Version). CoRR abs/2402.01428 (2024) - [i14]Ryan Kavanagh, Brigitte Pientka:
Message-Observing Sessions. CoRR abs/2403.04633 (2024) - 2023
- [j20]Jason Z. S. Hu, Junyoung Jang, Brigitte Pientka:
Normalization by evaluation for modal dependent type theory. J. Funct. Program. 33 (2023) - [j19]Chuta Sano, Ryan Kavanagh, Brigitte Pientka:
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity. Proc. ACM Program. Lang. 7(OOPSLA2): 374-399 (2023) - [c62]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: 750-756 - [e7]Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. ACM 2023 [contents] - [i13]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 abs/2301.02611 (2023) - [i12]Chuqin Geng, Yihan Zhang, Brigitte Pientka, Xujie Si:
Can ChatGPT Pass An Introductory Level Functional Language Programming Course? CoRR abs/2305.02230 (2023) - [i11]Jason Z. S. Hu, Brigitte Pientka:
Layered Modal Type Theories. CoRR abs/2305.06548 (2023) - [i10]Chuta Sano, Ryan Kavanagh, Brigitte Pientka:
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity. CoRR abs/2309.12466 (2023) - 2022
- [j18]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): 1-27 (2022) - [j17]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): 25:1-25:36 (2022) - [c59]Chuqin Geng, Haolin Ye, Yixuan Li, Tianyu Han, Brigitte Pientka, Xujie Si:
Novice Type Error Diagnosis with Natural Language Models. APLAS 2022: 196-214 - [c58]Jason Z. S. Hu, Brigitte Pientka:
A Categorical Normalization Proof for the Modal Lambda-Calculus. MFPS 2022 - [i9]Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp:
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types. CoRR abs/2206.02831 (2022) - [i8]Jason Z. S. Hu, Brigitte Pientka:
An Investigation of Kripke-style Modal Type Theories. CoRR abs/2206.07823 (2022) - [i7]Chuqin Geng, Haolin Ye, Yixuan Li, Tianyu Han, Brigitte Pientka, Xujie Si:
Novice Type Error Diagnosis with Natural Language Models. CoRR abs/2210.03682 (2022) - 2021
- [c57]Jacob Errington, Junyoung Jang, Brigitte Pientka:
Harpoon: Mechanizing Metatheory Interactively - (System Description). CADE 2021: 636-648 - [c56]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: 1341 - [i6]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 abs/2111.08099 (2021) - 2020
- [c55]Brigitte Pientka, Ulrich Schöpp:
Semantical Analysis of Contextual Types. FoSSaCS 2020: 502-521 - 2019
- [j16]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: e19 (2019) - [j15]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) - [j14]Aliya Hameer, Brigitte Pientka:
Teaching the art of functional programming using automated grading (experience report). Proc. ACM Program. Lang. 3(ICFP): 115:1-115:15 (2019) - [c52]Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini:
A Type Theory for Defining Logics and Proofs. LICS 2019: 1-13 - [i5]Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rébecca Zucchini:
Cocon: Computation in Contextual Type Theory. CoRR abs/1901.03378 (2019) - [i4]Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini:
A Type Theory for Defining Logics and Proofs. CoRR abs/1905.02617 (2019) - 2018
- [j13]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): 1507-1540 (2018) - [j12]Andrew Cave, Brigitte Pientka:
Mechanizing proofs with logical relations - Kripke-style. Math. Struct. Comput. Sci. 28(9): 1606-1638 (2018) - [c50]Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau:
Index-Stratified Types. FSCD 2018: 19:1-19:17 - [i3]Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau:
Index-Stratified Types (Extended Version). CoRR abs/1805.00401 (2018) - 2017
- [c49]Francisco Ferreira, Brigitte Pientka:
Programs Using Syntax with First-Class Binders. ESOP 2017: 504-529 - [c48]Aïna Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka:
LINCX: A Linear Logical Framework with First-Class Contexts. ESOP 2017: 530-555 - [c47]Jonas Kaiser, Brigitte Pientka, Gert Smolka:
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. FSCD 2017: 21:1-21:19 - 2016
- [j11]Andreas Abel, Brigitte Pientka:
Well-founded recursion with copatterns and sized types. J. Funct. Program. 26: e2 (2016) - [c46]David Thibodeau, Andrew Cave, Brigitte Pientka:
Indexed codata types. ICFP 2016: 351-363 - [c45]Rohan Jacob-Rao, Andrew Cave, Brigitte Pientka:
Mechanizing Proofs about Mendler-style Recursion. LFMTP 2016: 1:1-1:9 - [i2]Gilles Dowek, Catherine Dubois, Brigitte Pientka, Florian Rabe:
Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports 6(10): 75-98 (2016) - 2015
- [j10]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): 307-372 (2015) - [j9]Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka:
Programming type-safe transformations using higher-order abstract syntax. J. Formaliz. Reason. 8(1): 49-91 (2015) - [c44]Brigitte Pientka, Andrew Cave:
Inductive Beluga: Programming Proofs. CADE 2015: 272-281 - [c42]Brigitte Pientka, Andreas Abel:
Well-Founded Recursion over Contextual Objects. TLCA 2015: 273-287 - [c41]Amy P. Felty, Alberto Momigliano, Brigitte Pientka:
An Open Challenge Problem Repository for Systems Supporting Binders. LFMTP 2015: 18-32 - [c40]Andrew Cave, Brigitte Pientka:
A Case Study on Logical Relations using Contextual Types. LFMTP 2015: 33-45 - [i1]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 abs/1503.06095 (2015) - 2014
- [c39]Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka:
Fair reactive programming. POPL 2014: 361-372 - [c38]Francisco Ferreira, Brigitte Pientka:
Bidirectional Elaboration of Dependently Typed Programs. PPDP 2014: 161-174 - [c37]Anton Setzer, Andreas Abel, Brigitte Pientka, David Thibodeau:
Unnesting of Copatterns. RTA-TLCA 2014: 31-45 - [e4]Amy P. Felty, Brigitte Pientka:
Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014. ACM 2014, ISBN 978-1-4503-2817-3 [contents] - 2013
- [c36]Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka:
Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. CPP 2013: 243-258 - [c35]Andreas Abel, Brigitte Pientka:
Wellfounded recursion with copatterns: a unified approach to termination and productivity. ICFP 2013: 185-196 - [c34]Andrew Cave, Brigitte Pientka:
First-class substitutions in contextual type theory. LFMTP 2013: 15-24 - [c33]Francisco Ferreira, Stefan Monnier, Brigitte Pientka:
Compiling contextual objects: bringing higher-order abstract syntax to programmers. PLPV 2013: 13-24 - [c32]Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer:
Copatterns: programming infinite structures by observations. POPL 2013: 27-38 - [e3]Alberto Momigliano, Brigitte Pientka, Randy Pollack:
Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013. ACM 2013, ISBN 978-1-4503-2382-6 [contents] - 2012
- [c31]Andrew Cave, Brigitte Pientka:
Programming with binders and indexed data-types. POPL 2012: 413-424 - 2011
- [j7]Valeria de Paiva, Brigitte Pientka:
Intuitionistic Modal Logic and Applications (IMLA 2008). Inf. Comput. 209(12): 1435-1436 (2011) - [c30]Andreas Abel, Brigitte Pientka:
Higher-Order Dynamic Pattern Unification for Dependent Types and Records. TLCA 2011: 10-26 - 2010
- [c27]Brigitte Pientka, Jana Dunfield:
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). IJCAR 2010: 15-21 - [c25]Amy P. Felty, Brigitte Pientka:
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. ITP 2010: 227-242 - [c24]Andreas Abel, Brigitte Pientka:
Explicit Substitutions for Contextual Type Theory. LFMTP 2010: 5-20 - 2008
- [j4]Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka:
Contextual modal type theory. ACM Trans. Comput. Log. 9(3): 23:1-23:49 (2008) - [c22]Brigitte Pientka, Jana Dunfield:
Programming with proofs and explicit contexts. PPDP 2008: 163-173 - [c21]Jana Dunfield, Brigitte Pientka:
Case Analysis of Higher-Order Data. LFMTP@LICS 2008: 69-84 - [e2]Brigitte Pientka, Carsten Schürmann:
Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007. Electronic Notes in Theoretical Computer Science 196, Elsevier 2008 [contents] - 2007
- [c18]Brigitte Pientka, Carsten Schürmann:
Preface. LFMTP@CADE 2007: 1 - [c17]Brigitte Pientka, Xi Li, Florent Pompigne:
Focusing the Inverse Method for LF: A Preliminary Report. LFMTP@CADE 2007: 95-112 - [e1]Alberto Momigliano, Brigitte Pientka:
Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006. Electronic Notes in Theoretical Computer Science 174(5), Elsevier 2007 [contents] - 2006
- [c14]Alberto Momigliano, Brigitte Pientka:
Preface. LFMTP@FLoC 2006: 1-2 - 2005
- [c11]Susmit Sarkar, Brigitte Pientka, Karl Crary:
Small Proof Witnesses for LF. ICLP 2005: 387-401 - 2003
- [c10]Brigitte Pientka, Frank Pfenning:
Optimizing Higher-Order Pattern Unification. CADE 2003: 473-487 - [c9]Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning:
A modal foundation for meta-variables. MERLIN 2003
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-19 19:30 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint