Stop the war!
Остановите войну!
for scientists:
default search action
BibTeX records: Brigitte Pientka
@proceedings{DBLP:conf/cpp/2024, editor = {Amin Timany and Dmitriy Traytel and Brigitte Pientka and Sandrine Blazy}, title = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16, 2024}, publisher = {{ACM}}, year = {2024}, url = {https://doi.org/10.1145/3636501}, doi = {10.1145/3636501}, timestamp = {Thu, 11 Jan 2024 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/2024.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2402-01428, author = {Junyoung Jang and Sophia Roshal and Frank Pfenning and Brigitte Pientka}, title = {Adjoint Natural Deduction (Extended Version)}, journal = {CoRR}, volume = {abs/2402.01428}, year = {2024}, url = {https://doi.org/10.48550/arXiv.2402.01428}, doi = {10.48550/ARXIV.2402.01428}, eprinttype = {arXiv}, eprint = {2402.01428}, timestamp = {Fri, 09 Feb 2024 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2402-01428.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jfp/HuJP23, author = {Jason Z. S. Hu and Junyoung Jang and Brigitte Pientka}, title = {Normalization by evaluation for modal dependent type theory}, journal = {J. Funct. Program.}, volume = {33}, year = {2023}, url = {https://doi.org/10.1017/s0956796823000060}, doi = {10.1017/S0956796823000060}, timestamp = {Thu, 21 Mar 2024 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/jfp/HuJP23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/pacmpl/SanoKP23, author = {Chuta Sano and Ryan Kavanagh and Brigitte Pientka}, title = {Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity}, journal = {Proc. {ACM} Program. Lang.}, volume = {7}, number = {{OOPSLA2}}, pages = {374--399}, year = {2023}, url = {https://doi.org/10.1145/3622810}, doi = {10.1145/3622810}, timestamp = {Sun, 10 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/pacmpl/SanoKP23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/sigcse/GengXXPS23, author = {Chuqin Geng and Wenwen Xu and Yingjie Xu and Brigitte Pientka and Xujie Si}, editor = {Maureen Doyle and Ben Stephenson and Brian Dorn and Leen{-}Kiat Soh and Lina Battestilli}, title = {Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students}, booktitle = {Proceedings of the 54th {ACM} Technical Symposium on Computer Science Education, Volume 1, {SIGCSE} 2023, Toronto, ON, Canada, March 15-18, 2023}, pages = {750--756}, publisher = {{ACM}}, year = {2023}, url = {https://doi.org/10.1145/3545945.3569882}, doi = {10.1145/3545945.3569882}, timestamp = {Sat, 11 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/sigcse/GengXXPS23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2311-10577, author = {Antoine Gaulin and Brigitte Pientka}, editor = {Alberto Ciaffaglione and Carlos Olarte}, title = {Contextual Refinement Types}, booktitle = {Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023}, series = {{EPTCS}}, volume = {396}, pages = {4--19}, year = {2023}, url = {https://doi.org/10.4204/EPTCS.396.2}, doi = {10.4204/EPTCS.396.2}, timestamp = {Fri, 22 Dec 2023 16:43:30 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2311-10577.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2311-10439, author = {Johanna Schwartzentruber and Brigitte Pientka}, editor = {Alberto Ciaffaglione and Carlos Olarte}, title = {Semi-Automation of Meta-Theoretic Proofs in Beluga}, booktitle = {Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023}, series = {{EPTCS}}, volume = {396}, pages = {20--35}, year = {2023}, url = {https://doi.org/10.4204/EPTCS.396.3}, doi = {10.4204/EPTCS.396.3}, timestamp = {Fri, 22 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2311-10439.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/cade/2023, editor = {Brigitte Pientka and Cesare Tinelli}, title = {Automated Deduction - {CADE} 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {14132}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-38499-8}, doi = {10.1007/978-3-031-38499-8}, isbn = {978-3-031-38498-1}, timestamp = {Tue, 12 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/2023.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/cpp/2023, editor = {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka and Steve Zdancewic}, title = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January 16-17, 2023}, publisher = {{ACM}}, year = {2023}, url = {https://doi.org/10.1145/3573105}, doi = {10.1145/3573105}, timestamp = {Fri, 13 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/2023.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2301-02611, author = {Chuqin Geng and Wenwen Xu and Yingjie Xu and Brigitte Pientka and Xujie Si}, title = {Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students}, journal = {CoRR}, volume = {abs/2301.02611}, year = {2023}, url = {https://doi.org/10.48550/arXiv.2301.02611}, doi = {10.48550/ARXIV.2301.02611}, eprinttype = {arXiv}, eprint = {2301.02611}, timestamp = {Tue, 10 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2301-02611.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2305-02230, author = {Chuqin Geng and Yihan Zhang and Brigitte Pientka and Xujie Si}, title = {Can ChatGPT Pass An Introductory Level Functional Language Programming Course?}, journal = {CoRR}, volume = {abs/2305.02230}, year = {2023}, url = {https://doi.org/10.48550/arXiv.2305.02230}, doi = {10.48550/ARXIV.2305.02230}, eprinttype = {arXiv}, eprint = {2305.02230}, timestamp = {Wed, 10 May 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2305-02230.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2305-06548, author = {Jason Z. S. Hu and Brigitte Pientka}, title = {Layered Modal Type Theories}, journal = {CoRR}, volume = {abs/2305.06548}, year = {2023}, url = {https://doi.org/10.48550/arXiv.2305.06548}, doi = {10.48550/ARXIV.2305.06548}, eprinttype = {arXiv}, eprint = {2305.06548}, timestamp = {Tue, 16 May 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2305-06548.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2309-12466, author = {Chuta Sano and Ryan Kavanagh and Brigitte Pientka}, title = {Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity}, journal = {CoRR}, volume = {abs/2309.12466}, year = {2023}, url = {https://doi.org/10.48550/arXiv.2309.12466}, doi = {10.48550/ARXIV.2309.12466}, eprinttype = {arXiv}, eprint = {2309.12466}, timestamp = {Wed, 27 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2309-12466.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/pacmpl/JangGMP22, author = {Junyoung Jang and Samuel G{\'{e}}lineau and Stefan Monnier and Brigitte Pientka}, title = {M{\oe}bius: metaprogramming using contextual types: the stage where system f can pattern match on itself}, journal = {Proc. {ACM} Program. Lang.}, volume = {6}, number = {{POPL}}, pages = {1--27}, year = {2022}, url = {https://doi.org/10.1145/3498700}, doi = {10.1145/3498700}, timestamp = {Mon, 05 Dec 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/pacmpl/JangGMP22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/tocl/HuPS22, author = {Jason Z. S. Hu and Brigitte Pientka and Ulrich Sch{\"{o}}pp}, title = {A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types}, journal = {{ACM} Trans. Comput. Log.}, volume = {23}, number = {4}, pages = {25:1--25:36}, year = {2022}, url = {https://doi.org/10.1145/3545115}, doi = {10.1145/3545115}, timestamp = {Mon, 05 Dec 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/tocl/HuPS22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/aplas/GengYLHPS22, author = {Chuqin Geng and Haolin Ye and Yixuan Li and Tianyu Han and Brigitte Pientka and Xujie Si}, editor = {Ilya Sergey}, title = {Novice Type Error Diagnosis with Natural Language Models}, booktitle = {Programming Languages and Systems - 20th Asian Symposium, {APLAS} 2022, Auckland, New Zealand, December 5, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13658}, pages = {196--214}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-21037-2\_10}, doi = {10.1007/978-3-031-21037-2\_10}, timestamp = {Mon, 05 Dec 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/aplas/GengYLHPS22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2211-12318, author = {Jason Z. S. Hu and Brigitte Pientka}, editor = {Justin Hsu and Christine Tasson}, title = {A Categorical Normalization Proof for the Modal Lambda-Calculus}, booktitle = {Proceedings of the 38th Conference on the Mathematical Foundations of Programming Semantics, {MFPS} XXXXVIII, Cornell University, Ithaca, NY, USA, with a satellite event at IRIF, Denis Diderot University, Paris, France, and online, July 11-13, 2022}, series = {{EPTICS}}, volume = {1}, publisher = {EpiSciences}, year = {2022}, url = {https://doi.org/10.46298/entics.10360}, doi = {10.46298/ENTICS.10360}, timestamp = {Wed, 24 Jan 2024 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2211-12318.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2206-02831, author = {Jason Z. S. Hu and Brigitte Pientka and Ulrich Sch{\"{o}}pp}, title = {A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types}, journal = {CoRR}, volume = {abs/2206.02831}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2206.02831}, doi = {10.48550/ARXIV.2206.02831}, eprinttype = {arXiv}, eprint = {2206.02831}, timestamp = {Tue, 14 Jun 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2206-02831.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2206-07823, author = {Jason Z. S. Hu and Brigitte Pientka}, title = {An Investigation of Kripke-style Modal Type Theories}, journal = {CoRR}, volume = {abs/2206.07823}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2206.07823}, doi = {10.48550/ARXIV.2206.07823}, eprinttype = {arXiv}, eprint = {2206.07823}, timestamp = {Tue, 21 Jun 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2206-07823.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2210-03682, author = {Chuqin Geng and Haolin Ye and Yixuan Li and Tianyu Han and Brigitte Pientka and Xujie Si}, title = {Novice Type Error Diagnosis with Natural Language Models}, journal = {CoRR}, volume = {abs/2210.03682}, year = {2022}, url = {https://doi.org/10.48550/arXiv.2210.03682}, doi = {10.48550/ARXIV.2210.03682}, eprinttype = {arXiv}, eprint = {2210.03682}, timestamp = {Wed, 12 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2210-03682.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/ErringtonJP21, author = {Jacob Errington and Junyoung Jang and Brigitte Pientka}, editor = {Andr{\'{e}} Platzer and Geoff Sutcliffe}, title = {Harpoon: Mechanizing Metatheory Interactively - (System Description)}, booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {12699}, pages = {636--648}, publisher = {Springer}, year = {2021}, url = {https://doi.org/10.1007/978-3-030-79876-5\_38}, doi = {10.1007/978-3-030-79876-5\_38}, timestamp = {Tue, 02 Aug 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cade/ErringtonJP21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/sigcse/CeciTPS21, author = {Alana Ceci and Hanneli C. A. Tavante and Brigitte Pientka and Xujie Si}, editor = {Mark Sherriff and Laurence D. Merkle and Pamela A. Cutter and Alvaro E. Monge and Judithe Sheard}, title = {Data Collection for the Learn-OCaml Programming Platform: Modelling How Students Develop Typed Functional Programs}, booktitle = {{SIGCSE} '21: The 52nd {ACM} Technical Symposium on Computer Science Education, Virtual Event, USA, March 13-20, 2021}, pages = {1341}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3408877.3439579}, doi = {10.1145/3408877.3439579}, timestamp = {Wed, 07 Apr 2021 16:26:26 +0200}, biburl = {https://dblp.org/rec/conf/sigcse/CeciTPS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-2111-08099, author = {Junyoung Jang and Samuel G{\'{e}}lineau and Stefan Monnier and Brigitte Pientka}, title = {Moebius: Metaprogramming using Contextual Types - The stage where System {F} can pattern match on itself (Long Version)}, journal = {CoRR}, volume = {abs/2111.08099}, year = {2021}, url = {https://arxiv.org/abs/2111.08099}, eprinttype = {arXiv}, eprint = {2111.08099}, timestamp = {Tue, 02 Aug 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2111-08099.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fossacs/PientkaS20, author = {Brigitte Pientka and Ulrich Sch{\"{o}}pp}, editor = {Jean Goubault{-}Larrecq and Barbara K{\"{o}}nig}, title = {Semantical Analysis of Contextual Types}, booktitle = {Foundations of Software Science and Computation Structures - 23rd International Conference, {FOSSACS} 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2020, Dublin, Ireland, April 25-30, 2020, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {12077}, pages = {502--521}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-45231-5\_26}, doi = {10.1007/978-3-030-45231-5\_26}, timestamp = {Sat, 09 Apr 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fossacs/PientkaS20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/fscd/Pientka20, author = {Brigitte Pientka}, editor = {Zena M. Ariola}, title = {A Modal Analysis of Metaprogramming, Revisited (Invited Talk)}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)}, series = {LIPIcs}, volume = {167}, pages = {2:1--2:3}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2020}, url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.2}, doi = {10.4230/LIPICS.FSCD.2020.2}, timestamp = {Tue, 30 Jun 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/fscd/Pientka20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lics/Pientka20, author = {Brigitte Pientka}, editor = {Holger Hermanns and Lijun Zhang and Naoki Kobayashi and Dale Miller}, title = {Contextual Types, Explained: Invited Tutorial}, booktitle = {{LICS} '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer Science, Saarbr{\"{u}}cken, Germany, July 8-11, 2020}, pages = {35--37}, publisher = {{ACM}}, year = {2020}, url = {https://doi.org/10.1145/3373718.3394735}, doi = {10.1145/3373718.3394735}, timestamp = {Sat, 30 Sep 2023 09:52:07 +0200}, biburl = {https://dblp.org/rec/conf/lics/Pientka20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jfp/AbelAHPMSS19, author = {Andreas Abel and Guillaume Allais and Aliya Hameer and Brigitte Pientka and Alberto Momigliano and Steven Sch{\"{a}}fer and Kathrin Stark}, title = {POPLMark reloaded: Mechanizing proofs by logical relations}, journal = {J. Funct. Program.}, volume = {29}, pages = {e19}, year = {2019}, url = {https://doi.org/10.1017/S0956796819000170}, doi = {10.1017/S0956796819000170}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/AbelAHPMSS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/mscs/MomiglianoPT19, author = {Alberto Momigliano and Brigitte Pientka and David Thibodeau}, title = {A case study in programming coinductive proofs: Howe's method}, journal = {Math. Struct. Comput. Sci.}, volume = {29}, number = {8}, pages = {1309--1343}, year = {2019}, url = {https://doi.org/10.1017/S0960129518000415}, doi = {10.1017/S0960129518000415}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/mscs/MomiglianoPT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/pacmpl/HameerP19, author = {Aliya Hameer and Brigitte Pientka}, title = {Teaching the art of functional programming using automated grading (experience report)}, journal = {Proc. {ACM} Program. Lang.}, volume = {3}, number = {{ICFP}}, pages = {115:1--115:15}, year = {2019}, url = {https://doi.org/10.1145/3341719}, doi = {10.1145/3341719}, timestamp = {Wed, 17 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/pacmpl/HameerP19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lics/PientkaT00Z19, author = {Brigitte Pientka and David Thibodeau and Andreas Abel and Francisco Ferreira and R{\'{e}}becca Zucchini}, title = {A Type Theory for Defining Logics and Proofs}, booktitle = {34th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS} 2019, Vancouver, BC, Canada, June 24-27, 2019}, pages = {1--13}, publisher = {{IEEE}}, year = {2019}, url = {https://doi.org/10.1109/LICS.2019.8785683}, doi = {10.1109/LICS.2019.8785683}, timestamp = {Thu, 21 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lics/PientkaT00Z19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1901-03378, author = {Brigitte Pientka and Andreas Abel and Francisco Ferreira and David Thibodeau and R{\'{e}}becca Zucchini}, title = {Cocon: Computation in Contextual Type Theory}, journal = {CoRR}, volume = {abs/1901.03378}, year = {2019}, url = {http://arxiv.org/abs/1901.03378}, eprinttype = {arXiv}, eprint = {1901.03378}, timestamp = {Thu, 21 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1901-03378.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1905-02617, author = {Brigitte Pientka and David Thibodeau and Andreas Abel and Francisco Ferreira and R{\'{e}}becca Zucchini}, title = {A Type Theory for Defining Logics and Proofs}, journal = {CoRR}, volume = {abs/1905.02617}, year = {2019}, url = {http://arxiv.org/abs/1905.02617}, eprinttype = {arXiv}, eprint = {1905.02617}, timestamp = {Thu, 21 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1905-02617.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/mscs/FeltyMP18, author = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka}, title = {Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions}, journal = {Math. Struct. Comput. Sci.}, volume = {28}, number = {9}, pages = {1507--1540}, year = {2018}, url = {https://doi.org/10.1017/S0960129517000093}, doi = {10.1017/S0960129517000093}, timestamp = {Wed, 01 Apr 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/mscs/FeltyMP18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/mscs/CaveP18, author = {Andrew Cave and Brigitte Pientka}, title = {Mechanizing proofs with logical relations - Kripke-style}, journal = {Math. Struct. Comput. Sci.}, volume = {28}, number = {9}, pages = {1606--1638}, year = {2018}, url = {https://doi.org/10.1017/S0960129518000154}, doi = {10.1017/S0960129518000154}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/mscs/CaveP18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/Pientka18, author = {Brigitte Pientka}, editor = {June Andronick and Amy P. Felty}, title = {POPLMark reloaded: mechanizing logical relations proofs (invited talk)}, booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January 8-9, 2018}, pages = {1}, publisher = {{ACM}}, year = {2018}, url = {https://doi.org/10.1145/3167102}, doi = {10.1145/3167102}, timestamp = {Wed, 21 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/Pientka18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/rta/Jacob-RaoPT18, author = {Rohan Jacob{-}Rao and Brigitte Pientka and David Thibodeau}, editor = {H{\'{e}}l{\`{e}}ne Kirchner}, title = {Index-Stratified Types}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction, {FSCD} 2018, July 9-12, 2018, Oxford, {UK}}, series = {LIPIcs}, volume = {108}, pages = {19:1--19:17}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2018}, url = {https://doi.org/10.4230/LIPIcs.FSCD.2018.19}, doi = {10.4230/LIPICS.FSCD.2018.19}, timestamp = {Thu, 21 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/rta/Jacob-RaoPT18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/abs-1805-00401, author = {Rohan Jacob{-}Rao and Brigitte Pientka and David Thibodeau}, title = {Index-Stratified Types (Extended Version)}, journal = {CoRR}, volume = {abs/1805.00401}, year = {2018}, url = {http://arxiv.org/abs/1805.00401}, eprinttype = {arXiv}, eprint = {1805.00401}, timestamp = {Thu, 21 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1805-00401.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/esop/0001P17, author = {Francisco Ferreira and Brigitte Pientka}, editor = {Hongseok Yang}, title = {Programs Using Syntax with First-Class Binders}, booktitle = {Programming Languages and Systems - 26th European Symposium on Programming, {ESOP} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10201}, pages = {504--529}, publisher = {Springer}, year = {2017}, url = {https://doi.org/10.1007/978-3-662-54434-1\_19}, doi = {10.1007/978-3-662-54434-1\_19}, timestamp = {Tue, 14 May 2019 10:00:41 +0200}, biburl = {https://dblp.org/rec/conf/esop/0001P17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/esop/GeorgesMOP17, author = {A{\"{\i}}na Linn Georges and Agata Murawska and Shawn Otis and Brigitte Pientka}, editor = {Hongseok Yang}, title = {{LINCX:} {A} Linear Logical Framework with First-Class Contexts}, booktitle = {Programming Languages and Systems - 26th European Symposium on Programming, {ESOP} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10201}, pages = {530--555}, publisher = {Springer}, year = {2017}, url = {https://doi.org/10.1007/978-3-662-54434-1\_20}, doi = {10.1007/978-3-662-54434-1\_20}, timestamp = {Wed, 20 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/esop/GeorgesMOP17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/rta/KaiserPS17, author = {Jonas Kaiser and Brigitte Pientka and Gert Smolka}, editor = {Dale Miller}, title = {Relating System {F} and Lambda2: {A} Case Study in Coq, Abella and Beluga}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction, {FSCD} 2017, September 3-9, 2017, Oxford, {UK}}, series = {LIPIcs}, volume = {84}, pages = {21:1--21:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2017}, url = {https://doi.org/10.4230/LIPIcs.FSCD.2017.21}, doi = {10.4230/LIPICS.FSCD.2017.21}, timestamp = {Tue, 11 Feb 2020 15:52:14 +0100}, biburl = {https://dblp.org/rec/conf/rta/KaiserPS17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/ppdp/2017, editor = {Wim Vanhoof and Brigitte Pientka}, title = {Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017}, publisher = {{ACM}}, year = {2017}, url = {http://dl.acm.org/citation.cfm?id=3131851}, isbn = {978-1-4503-5291-8}, timestamp = {Mon, 20 Nov 2017 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/ppdp/2017.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jfp/0001P16, author = {Andreas Abel and Brigitte Pientka}, title = {Well-founded recursion with copatterns and sized types}, journal = {J. Funct. Program.}, volume = {26}, pages = {e2}, year = {2016}, url = {https://doi.org/10.1017/S0956796816000022}, doi = {10.1017/S0956796816000022}, timestamp = {Sat, 27 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/0001P16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/icfp/ThibodeauCP16, author = {David Thibodeau and Andrew Cave and Brigitte Pientka}, editor = {Jacques Garrigue and Gabriele Keller and Eijiro Sumii}, title = {Indexed codata types}, booktitle = {Proceedings of the 21st {ACM} {SIGPLAN} International Conference on Functional Programming, {ICFP} 2016, Nara, Japan, September 18-22, 2016}, pages = {351--363}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2951913.2951929}, doi = {10.1145/2951913.2951929}, timestamp = {Wed, 23 Jun 2021 15:34:31 +0200}, biburl = {https://dblp.org/rec/conf/icfp/ThibodeauCP16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Jacob-RaoCP16, author = {Rohan Jacob{-}Rao and Andrew Cave and Brigitte Pientka}, editor = {Gilles Dowek and Daniel R. Licata and Sandra Alves}, title = {Mechanizing Proofs about Mendler-style Recursion}, booktitle = {Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2016, Porto, Portugal, June 23, 2016}, pages = {1:1--1:9}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2966268.2966269}, doi = {10.1145/2966268.2966269}, timestamp = {Tue, 06 Nov 2018 16:57:31 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Jacob-RaoCP16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/rta/2016, editor = {Delia Kesner and Brigitte Pientka}, title = {1st International Conference on Formal Structures for Computation and Deduction, {FSCD} 2016, June 22-26, 2016, Porto, Portugal}, series = {LIPIcs}, volume = {52}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2016}, url = {http://www.dagstuhl.de/dagpub/978-3-95977-010-1}, isbn = {978-3-95977-010-1}, timestamp = {Tue, 11 Feb 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/rta/2016.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/dagstuhl-reports/DowekDPR16, author = {Gilles Dowek and Catherine Dubois and Brigitte Pientka and Florian Rabe}, title = {Universality of Proofs (Dagstuhl Seminar 16421)}, journal = {Dagstuhl Reports}, volume = {6}, number = {10}, pages = {75--98}, year = {2016}, url = {https://doi.org/10.4230/DagRep.6.10.75}, doi = {10.4230/DAGREP.6.10.75}, timestamp = {Fri, 20 Nov 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/dagstuhl-reports/DowekDPR16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/FeltyMP15, author = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka}, title = {The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - {A} Survey}, journal = {J. Autom. Reason.}, volume = {55}, number = {4}, pages = {307--372}, year = {2015}, url = {https://doi.org/10.1007/s10817-015-9327-3}, doi = {10.1007/S10817-015-9327-3}, timestamp = {Wed, 02 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jar/FeltyMP15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jfrea/BelangerMP15, author = {Olivier Savary B{\'{e}}langer and Stefan Monnier and Brigitte Pientka}, title = {Programming type-safe transformations using higher-order abstract syntax}, journal = {J. Formaliz. Reason.}, volume = {8}, number = {1}, pages = {49--91}, year = {2015}, url = {https://doi.org/10.6092/issn.1972-5787/5122}, doi = {10.6092/ISSN.1972-5787/5122}, timestamp = {Thu, 24 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfrea/BelangerMP15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/PientkaC15, author = {Brigitte Pientka and Andrew Cave}, editor = {Amy P. Felty and Aart Middeldorp}, title = {Inductive Beluga: Programming Proofs}, booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9195}, pages = {272--281}, publisher = {Springer}, year = {2015}, url = {https://doi.org/10.1007/978-3-319-21401-6\_18}, doi = {10.1007/978-3-319-21401-6\_18}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/PientkaC15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/rta/Pientka15, author = {Brigitte Pientka}, editor = {Yuki Chiba and Santiago Escobar and Naoki Nishida and David Sabel and Manfred Schmidt{-}Schau{\ss}}, title = {Mechanizing Meta-Theory in Beluga (Invited Talk)}, booktitle = {2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE@RDP 2015, July 2, 2015, Warsaw, Poland}, series = {OASIcs}, volume = {46}, pages = {1--1}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2015}, url = {https://doi.org/10.4230/OASIcs.WPTE.2015.1}, doi = {10.4230/OASICS.WPTE.2015.1}, timestamp = {Fri, 03 Feb 2023 10:42:58 +0100}, biburl = {https://dblp.org/rec/conf/rta/Pientka15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tlca/Pientka015, author = {Brigitte Pientka and Andreas Abel}, editor = {Thorsten Altenkirch}, title = {Well-Founded Recursion over Contextual Objects}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications, {TLCA} 2015, July 1-3, 2015, Warsaw, Poland}, series = {LIPIcs}, volume = {38}, pages = {273--287}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2015}, url = {https://doi.org/10.4230/LIPIcs.TLCA.2015.273}, doi = {10.4230/LIPICS.TLCA.2015.273}, timestamp = {Tue, 11 Feb 2020 15:52:14 +0100}, biburl = {https://dblp.org/rec/conf/tlca/Pientka015.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/FeltyMP15a, author = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka}, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {An Open Challenge Problem Repository for Systems Supporting Binders}, booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, pages = {18--32}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185.2}, doi = {10.4204/EPTCS.185.2}, timestamp = {Wed, 12 Sep 2018 01:05:12 +0200}, biburl = {https://dblp.org/rec/journals/corr/FeltyMP15a.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/CaveP15, author = {Andrew Cave and Brigitte Pientka}, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {A Case Study on Logical Relations using Contextual Types}, booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, pages = {33--45}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185.3}, doi = {10.4204/EPTCS.185.3}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/CaveP15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/corr/FeltyMP15, author = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka}, title = {The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks}, journal = {CoRR}, volume = {abs/1503.06095}, year = {2015}, url = {http://arxiv.org/abs/1503.06095}, eprinttype = {arXiv}, eprint = {1503.06095}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/FeltyMP15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/popl/CaveFPP14, author = {Andrew Cave and Francisco Ferreira and Prakash Panangaden and Brigitte Pientka}, editor = {Suresh Jagannathan and Peter Sewell}, title = {Fair reactive programming}, booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21, 2014}, pages = {361--372}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2535838.2535881}, doi = {10.1145/2535838.2535881}, timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, biburl = {https://dblp.org/rec/conf/popl/CaveFPP14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/ppdp/FerreiraP14, author = {Francisco Ferreira and Brigitte Pientka}, editor = {Olaf Chitil and Andy King and Olivier Danvy}, title = {Bidirectional Elaboration of Dependently Typed Programs}, booktitle = {Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014}, pages = {161--174}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2643135.2643153}, doi = {10.1145/2643135.2643153}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/ppdp/FerreiraP14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/rta/Setzer0PT14, author = {Anton Setzer and Andreas Abel and Brigitte Pientka and David Thibodeau}, editor = {Gilles Dowek}, title = {Unnesting of Copatterns}, booktitle = {Rewriting and Typed Lambda Calculi - Joint International Conference, {RTA-TLCA} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 14-17, 2014. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8560}, pages = {31--45}, publisher = {Springer}, year = {2014}, url = {https://doi.org/10.1007/978-3-319-08918-8\_3}, doi = {10.1007/978-3-319-08918-8\_3}, timestamp = {Thu, 21 Jan 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/rta/Setzer0PT14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2014, editor = {Amy P. Felty and Brigitte Pientka}, title = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172}, doi = {10.1145/2631172}, isbn = {978-1-4503-2817-3}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2014.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jfp/Pientka13, author = {Brigitte Pientka}, title = {An insider's look at {LF} type reconstruction: everything you (n)ever wanted to know}, journal = {J. Funct. Program.}, volume = {23}, number = {1}, pages = {1--37}, year = {2013}, url = {https://doi.org/10.1017/S0956796812000408}, doi = {10.1017/S0956796812000408}, timestamp = {Sat, 27 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jfp/Pientka13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/BelangerMP13, author = {Olivier Savary B{\'{e}}langer and Stefan Monnier and Brigitte Pientka}, editor = {Georges Gonthier and Michael Norrish}, title = {Programming Type-Safe Transformations Using Higher-Order Abstract Syntax}, booktitle = {Certified Programs and Proofs - Third International Conference, {CPP} 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8307}, pages = {243--258}, publisher = {Springer}, year = {2013}, url = {https://doi.org/10.1007/978-3-319-03545-1\_16}, doi = {10.1007/978-3-319-03545-1\_16}, timestamp = {Tue, 14 May 2019 10:00:54 +0200}, biburl = {https://dblp.org/rec/conf/cpp/BelangerMP13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/icfp/AbelP13, author = {Andreas Abel and Brigitte Pientka}, editor = {Greg Morrisett and Tarmo Uustalu}, title = {Wellfounded recursion with copatterns: a unified approach to termination and productivity}, booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming, ICFP'13, Boston, MA, {USA} - September 25 - 27, 2013}, pages = {185--196}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2500365.2500591}, doi = {10.1145/2500365.2500591}, timestamp = {Thu, 24 Jun 2021 16:19:30 +0200}, biburl = {https://dblp.org/rec/conf/icfp/AbelP13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/CaveP13, author = {Andrew Cave and Brigitte Pientka}, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {First-class substitutions in contextual type theory}, booktitle = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, pages = {15--24}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887.2503889}, doi = {10.1145/2503887.2503889}, timestamp = {Tue, 06 Nov 2018 16:57:31 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/CaveP13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/plpv/FerreiraMP13, author = {Francisco Ferreira and Stefan Monnier and Brigitte Pientka}, editor = {Matthew Might and David Van Horn and Andreas Abel and Tim Sheard}, title = {Compiling contextual objects: bringing higher-order abstract syntax to programmers}, booktitle = {Proceedings of the 7th Workshop on Programming languages meets program verification, {PLPV} 2013, Rome, Italy, January 22, 2013}, pages = {13--24}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2428116.2428121}, doi = {10.1145/2428116.2428121}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/plpv/FerreiraMP13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/popl/AbelPTS13, author = {Andreas Abel and Brigitte Pientka and David Thibodeau and Anton Setzer}, editor = {Roberto Giacobazzi and Radhia Cousot}, title = {Copatterns: programming infinite structures by observations}, booktitle = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25, 2013}, pages = {27--38}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2429069.2429075}, doi = {10.1145/2429069.2429075}, timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, biburl = {https://dblp.org/rec/conf/popl/AbelPTS13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2013, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887}, doi = {10.1145/2503887}, isbn = {978-1-4503-2382-6}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2013.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/popl/CaveP12, author = {Andrew Cave and Brigitte Pientka}, editor = {John Field and Michael Hicks}, title = {Programming with binders and indexed data-types}, booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012}, pages = {413--424}, publisher = {{ACM}}, year = {2012}, url = {https://doi.org/10.1145/2103656.2103705}, doi = {10.1145/2103656.2103705}, timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, biburl = {https://dblp.org/rec/conf/popl/CaveP12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/iandc/PaivaP11, author = {Valeria de Paiva and Brigitte Pientka}, title = {Intuitionistic Modal Logic and Applications {(IMLA} 2008)}, journal = {Inf. Comput.}, volume = {209}, number = {12}, pages = {1435--1436}, year = {2011}, url = {https://doi.org/10.1016/j.ic.2011.10.004}, doi = {10.1016/J.IC.2011.10.004}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/iandc/PaivaP11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/SchmidtP11, author = {Renate A. Schmidt and Brigitte Pientka}, title = {Preface: Special Issue of Selected Extended Papers of {CADE-22}}, journal = {J. Autom. Reason.}, volume = {47}, number = {2}, pages = {107--109}, year = {2011}, url = {https://doi.org/10.1007/s10817-010-9212-z}, doi = {10.1007/S10817-010-9212-Z}, timestamp = {Wed, 02 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jar/SchmidtP11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tlca/AbelP11, author = {Andreas Abel and Brigitte Pientka}, editor = {C.{-}H. Luke Ong}, title = {Higher-Order Dynamic Pattern Unification for Dependent Types and Records}, booktitle = {Typed Lambda Calculi and Applications - 10th International Conference, {TLCA} 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6690}, pages = {10--26}, publisher = {Springer}, year = {2011}, url = {https://doi.org/10.1007/978-3-642-21691-6\_5}, doi = {10.1007/978-3-642-21691-6\_5}, timestamp = {Tue, 14 May 2019 10:00:41 +0200}, biburl = {https://dblp.org/rec/conf/tlca/AbelP11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1111-0087, author = {Mathieu Boespflug and Brigitte Pientka}, editor = {Herman Geuvers and Gopalan Nadathur}, title = {Multi-level Contextual Type Theory}, booktitle = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011}, series = {{EPTCS}}, volume = {71}, pages = {29--43}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.71.3}, doi = {10.4204/EPTCS.71.3}, timestamp = {Wed, 12 Sep 2018 01:05:13 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-0087.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/birthday/Pientka10, author = {Brigitte Pientka}, editor = {Simon Siegler and Nathan Wasser}, title = {Programming Inductive Proofs - {A} New Approach Based on Contextual Types}, booktitle = {Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday}, series = {Lecture Notes in Computer Science}, volume = {6463}, pages = {1--16}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-17172-7\_1}, doi = {10.1007/978-3-642-17172-7\_1}, timestamp = {Tue, 14 May 2019 10:00:52 +0200}, biburl = {https://dblp.org/rec/conf/birthday/Pientka10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/PientkaD10, author = {Brigitte Pientka and Jana Dunfield}, editor = {J{\"{u}}rgen Giesl and Reiner H{\"{a}}hnle}, title = {Beluga: {A} Framework for Programming and Reasoning with Deductive Systems (System Description)}, booktitle = {Automated Reasoning, 5th International Joint Conference, {IJCAR} 2010, Edinburgh, UK, July 16-19, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6173}, pages = {15--21}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14203-1\_2}, doi = {10.1007/978-3-642-14203-1\_2}, timestamp = {Fri, 11 Dec 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cade/PientkaD10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/flops/Pientka10, author = {Brigitte Pientka}, editor = {Matthias Blume and Naoki Kobayashi and Germ{\'{a}}n Vidal}, title = {Beluga: Programming with Dependent Types, Contextual Data, and Contexts}, booktitle = {Functional and Logic Programming, 10th International Symposium, {FLOPS} 2010, Sendai, Japan, April 19-21, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6009}, pages = {1--12}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-12251-4\_1}, doi = {10.1007/978-3-642-12251-4\_1}, timestamp = {Tue, 14 May 2019 10:00:53 +0200}, biburl = {https://dblp.org/rec/conf/flops/Pientka10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/FeltyP10, author = {Amy P. Felty and Brigitte Pientka}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Reasoning with Higher-Order Abstract Syntax and Contexts: {A} Comparison}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {227--242}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_17}, doi = {10.1007/978-3-642-14052-5\_17}, timestamp = {Tue, 14 May 2019 10:00:37 +0200}, biburl = {https://dblp.org/rec/conf/itp/FeltyP10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1009-2789, author = {Andreas Abel and Brigitte Pientka}, editor = {Karl Crary and Marino Miculan}, title = {Explicit Substitutions for Contextual Type Theory}, booktitle = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, pages = {5--20}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34.3}, doi = {10.4204/EPTCS.34.3}, timestamp = {Mon, 05 Feb 2024 20:18:33 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2789.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/tocl/Pientka09, author = {Brigitte Pientka}, title = {Higher-order term indexing using substitution trees}, journal = {{ACM} Trans. Comput. Log.}, volume = {11}, number = {1}, pages = {6:1--6:40}, year = {2009}, url = {https://doi.org/10.1145/1614431.1614437}, doi = {10.1145/1614431.1614437}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/tocl/Pientka09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/tocl/NanevskiPP08, author = {Aleksandar Nanevski and Frank Pfenning and Brigitte Pientka}, title = {Contextual modal type theory}, journal = {{ACM} Trans. Comput. Log.}, volume = {9}, number = {3}, pages = {23:1--23:49}, year = {2008}, url = {https://doi.org/10.1145/1352582.1352591}, doi = {10.1145/1352582.1352591}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/tocl/NanevskiPP08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/popl/Pientka08, author = {Brigitte Pientka}, editor = {George C. Necula and Philip Wadler}, title = {A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions}, booktitle = {Proceedings of the 35th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2008, San Francisco, California, USA, January 7-12, 2008}, pages = {371--382}, publisher = {{ACM}}, year = {2008}, url = {https://doi.org/10.1145/1328438.1328483}, doi = {10.1145/1328438.1328483}, timestamp = {Fri, 25 Jun 2021 14:48:54 +0200}, biburl = {https://dblp.org/rec/conf/popl/Pientka08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/ppdp/PientkaD08, author = {Brigitte Pientka and Jana Dunfield}, editor = {Sergio Antoy and Elvira Albert}, title = {Programming with proofs and explicit contexts}, booktitle = {Proceedings of the 10th International {ACM} {SIGPLAN} Conference on Principles and Practice of Declarative Programming, July 15-17, 2008, Valencia, Spain}, pages = {163--173}, publisher = {{ACM}}, year = {2008}, url = {https://doi.org/10.1145/1389449.1389469}, doi = {10.1145/1389449.1389469}, timestamp = {Fri, 11 Dec 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/ppdp/PientkaD08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/DunfieldP09, author = {Jana Dunfield and Brigitte Pientka}, editor = {Andreas Abel and Christian Urban}, title = {Case Analysis of Higher-Order Data}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {69--84}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.117}, doi = {10.1016/J.ENTCS.2008.12.117}, timestamp = {Fri, 24 Feb 2023 10:26:24 +0100}, biburl = {https://dblp.org/rec/journals/entcs/DunfieldP09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2007, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, publisher = {Elsevier}, year = {2008}, url = {https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/196/suppl/C}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2007.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/HeilalaP07, author = {Samuli Heilala and Brigitte Pientka}, editor = {Frank Pfenning}, title = {Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic {IS4}}, booktitle = {Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4603}, pages = {116--131}, publisher = {Springer}, year = {2007}, url = {https://doi.org/10.1007/978-3-540-73595-3\_9}, doi = {10.1007/978-3-540-73595-3\_9}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/HeilalaP07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tphol/Pientka07, author = {Brigitte Pientka}, editor = {Klaus Schneider and Jens Brandt}, title = {Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework {LF}}, booktitle = {Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4732}, pages = {246--261}, publisher = {Springer}, year = {2007}, url = {https://doi.org/10.1007/978-3-540-74591-4\_19}, doi = {10.1007/978-3-540-74591-4\_19}, timestamp = {Tue, 14 May 2019 10:00:48 +0200}, biburl = {https://dblp.org/rec/conf/tphol/Pientka07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/PientkaS08, author = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Preface}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {1}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.013}, doi = {10.1016/J.ENTCS.2007.09.013}, timestamp = {Thu, 09 Feb 2023 11:15:18 +0100}, biburl = {https://dblp.org/rec/journals/entcs/PientkaS08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/PientkaLP08, author = {Brigitte Pientka and Xi Li and Florent Pompigne}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Focusing the Inverse Method for {LF:} {A} Preliminary Report}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {95--112}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.020}, doi = {10.1016/J.ENTCS.2007.09.020}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/PientkaLP08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2006, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, publisher = {Elsevier}, year = {2007}, url = {https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/174/issue/5}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2006.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/Pientka06, author = {Brigitte Pientka}, editor = {Ulrich Furbach and Natarajan Shankar}, title = {Eliminating Redundancy in Higher-Order Unification: {A} Lightweight Approach}, booktitle = {Automated Reasoning, Third International Joint Conference, {IJCAR} 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4130}, pages = {362--376}, publisher = {Springer}, year = {2006}, url = {https://doi.org/10.1007/11814771\_32}, doi = {10.1007/11814771\_32}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/Pientka06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/iclp/Pientka06, author = {Brigitte Pientka}, editor = {Sandro Etalle and Miroslaw Truszczynski}, title = {Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks}, booktitle = {Logic Programming, 22nd International Conference, {ICLP} 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4079}, pages = {3--10}, publisher = {Springer}, year = {2006}, url = {https://doi.org/10.1007/11799573\_3}, doi = {10.1007/11799573\_3}, timestamp = {Tue, 14 May 2019 10:00:48 +0200}, biburl = {https://dblp.org/rec/conf/iclp/Pientka06.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/MomiglianoP07, author = {Alberto Momigliano and Brigitte Pientka}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Preface}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {1--2}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.015}, doi = {10.1016/J.ENTCS.2007.01.015}, timestamp = {Fri, 27 Jan 2023 13:31:48 +0100}, biburl = {https://dblp.org/rec/journals/entcs/MomiglianoP07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Pientka07, author = {Brigitte Pientka}, editor = {Aaron Stump and Hongwei Xi}, title = {Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions}, booktitle = {Proceedings of the Programming Languages meets Program Verification, PLPV@IJCAR 2006, Part of FLoC 2006, Seattle, WA, USA, August 21, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {7}, pages = {41--60}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2006.10.037}, doi = {10.1016/J.ENTCS.2006.10.037}, timestamp = {Fri, 27 Jan 2023 13:53:49 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Pientka07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/jar/Pientka05, author = {Brigitte Pientka}, title = {Verifying Termination and Reduction Properties about Higher-Order Logic Programs}, journal = {J. Autom. Reason.}, volume = {34}, number = {2}, pages = {179--207}, year = {2005}, url = {https://doi.org/10.1007/s10817-005-6534-3}, doi = {10.1007/S10817-005-6534-3}, timestamp = {Wed, 02 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/jar/Pientka05.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/Pientka05, author = {Brigitte Pientka}, editor = {Robert Nieuwenhuis}, title = {Tabling for Higher-Order Logic Programming}, booktitle = {Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {3632}, pages = {54--68}, publisher = {Springer}, year = {2005}, url = {https://doi.org/10.1007/11532231\_5}, doi = {10.1007/11532231\_5}, timestamp = {Sun, 02 Oct 2022 15:55:55 +0200}, biburl = {https://dblp.org/rec/conf/cade/Pientka05.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/iclp/SarkarPC05, author = {Susmit Sarkar and Brigitte Pientka and Karl Crary}, editor = {Maurizio Gabbrielli and Gopal Gupta}, title = {Small Proof Witnesses for {LF}}, booktitle = {Logic Programming, 21st International Conference, {ICLP} 2005, Sitges, Spain, October 2-5, 2005, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {3668}, pages = {387--401}, publisher = {Springer}, year = {2005}, url = {https://doi.org/10.1007/11562931\_29}, doi = {10.1007/11562931\_29}, timestamp = {Mon, 26 Jun 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/iclp/SarkarPC05.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/PientkaP03, author = {Brigitte Pientka and Frank Pfenning}, editor = {Franz Baader}, title = {Optimizing Higher-Order Pattern Unification}, booktitle = {Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {2741}, pages = {473--487}, publisher = {Springer}, year = {2003}, url = {https://doi.org/10.1007/978-3-540-45085-6\_40}, doi = {10.1007/978-3-540-45085-6\_40}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/PientkaP03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/icfp/NanevskiPP03, author = {Aleksandar Nanevski and Brigitte Pientka and Frank Pfenning}, title = {A modal foundation for meta-variables}, booktitle = {Eighth {ACM} {SIGPLAN} International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, {MERLIN} 2003, Uppsala, Sweden, August 2003}, publisher = {{ACM}}, year = {2003}, url = {https://doi.org/10.1145/976571.976582}, doi = {10.1145/976571.976582}, timestamp = {Mon, 12 Jul 2021 15:34:15 +0200}, biburl = {https://dblp.org/rec/conf/icfp/NanevskiPP03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/iclp/Pientka03, author = {Brigitte Pientka}, editor = {Catuscia Palamidessi}, title = {Higher-Order Substitution Tree Indexing}, booktitle = {Logic Programming, 19th International Conference, {ICLP} 2003, Mumbai, India, December 9-13, 2003, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {2916}, pages = {377--391}, publisher = {Springer}, year = {2003}, url = {https://doi.org/10.1007/978-3-540-24599-5\_26}, doi = {10.1007/978-3-540-24599-5\_26}, timestamp = {Tue, 14 May 2019 10:00:48 +0200}, biburl = {https://dblp.org/rec/conf/iclp/Pientka03.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/iclp/Pientka02, author = {Brigitte Pientka}, editor = {Peter J. Stuckey}, title = {A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming}, booktitle = {Logic Programming, 18th International Conference, {ICLP} 2002, Copenhagen, Denmark, July 29 - August 1, 2002, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {2401}, pages = {271--286}, publisher = {Springer}, year = {2002}, url = {https://doi.org/10.1007/3-540-45619-8\_19}, doi = {10.1007/3-540-45619-8\_19}, timestamp = {Tue, 14 May 2019 10:00:48 +0200}, biburl = {https://dblp.org/rec/conf/iclp/Pientka02.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Pientka02, author = {Brigitte Pientka}, editor = {Frank Pfenning}, title = {Memoization-Based Proof Search in {LF} - an Experimental Evaluation of a Prototype}, booktitle = {International Workshop on Logical Frameworks and Meta-Languages, {LFM} 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002}, series = {Electronic Notes in Theoretical Computer Science}, volume = {70}, number = {2}, pages = {110--123}, publisher = {Elsevier}, year = {2002}, url = {https://doi.org/10.1016/S1571-0661(04)80509-7}, doi = {10.1016/S1571-0661(04)80509-7}, timestamp = {Tue, 06 Dec 2022 14:32:51 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Pientka02.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/sLogica/KreitzP01, author = {Christoph Kreitz and Brigitte Pientka}, title = {Connection-Driven Inductive Theorem Proving}, journal = {Stud Logica}, volume = {69}, number = {2}, pages = {293--326}, year = {2001}, url = {https://doi.org/10.1023/A:1013874024997}, doi = {10.1023/A:1013874024997}, timestamp = {Tue, 01 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/sLogica/KreitzP01.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cade/Pientka01, author = {Brigitte Pientka}, editor = {Rajeev Gor{\'{e}} and Alexander Leitsch and Tobias Nipkow}, title = {Termination and Reduction Checking for Higher-Order Logic Programs}, booktitle = {Automated Reasoning, First International Joint Conference, {IJCAR} 2001, Siena, Italy, June 18-23, 2001, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {2083}, pages = {401--415}, publisher = {Springer}, year = {2001}, url = {https://doi.org/10.1007/3-540-45744-5\_32}, doi = {10.1007/3-540-45744-5\_32}, timestamp = {Tue, 14 May 2019 10:00:39 +0200}, biburl = {https://dblp.org/rec/conf/cade/Pientka01.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/birthday/KreitzOSP00, author = {Christoph Kreitz and Jens Otten and Stephan Schmitt and Brigitte Pientka}, editor = {Steffen H{\"{o}}lldobler}, title = {Matrix-based Constructive Theorem Proving}, booktitle = {Intellectics and Computational Logic (to Wolfgang Bibel on the occasion of his 60th birthday)}, series = {Applied Logic Series}, volume = {19}, pages = {189--205}, publisher = {Kluwer}, year = {2000}, timestamp = {Thu, 03 Jan 2002 11:54:05 +0100}, biburl = {https://dblp.org/rec/conf/birthday/KreitzOSP00.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/tableaux/KreitzP00, author = {Christoph Kreitz and Brigitte Pientka}, editor = {Roy Dyckhoff}, title = {Matrix-Based Inductive Theorem Proving}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, {TABLEAUX} 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {1847}, pages = {294--308}, publisher = {Springer}, year = {2000}, url = {https://doi.org/10.1007/10722086\_24}, doi = {10.1007/10722086\_24}, timestamp = {Tue, 14 May 2019 10:00:54 +0200}, biburl = {https://dblp.org/rec/conf/tableaux/KreitzP00.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@article{DBLP:journals/fuin/PientkaK99, author = {Brigitte Pientka and Christoph Kreitz}, title = {Automating Inductive Specification Proofs}, journal = {Fundam. Informaticae}, volume = {39}, number = {1-2}, pages = {189--209}, year = {1999}, url = {https://doi.org/10.3233/FI-1999-391210}, doi = {10.3233/FI-1999-391210}, timestamp = {Fri, 18 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/fuin/PientkaK99.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/aisc/PientkaK98, author = {Brigitte Pientka and Christoph Kreitz}, editor = {Jacques Calmet and Jan A. Plaza}, title = {Instantiation of Existentially Quantified Variables in Inductive Specification Proofs}, booktitle = {Artificial Intelligence and Symbolic Computation, International Conference AISC'98, Plattsburgh, New York, USA, September 16-18, 1998, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {1476}, pages = {247--258}, publisher = {Springer}, year = {1998}, url = {https://doi.org/10.1007/BFb0055917}, doi = {10.1007/BFB0055917}, timestamp = {Tue, 14 May 2019 10:00:52 +0200}, biburl = {https://dblp.org/rec/conf/aisc/PientkaK98.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/ki/GerberdingP97, author = {Stefan Gerberding and Brigitte Pientka}, editor = {Gerhard Brewka and Christopher Habel and Bernhard Nebel}, title = {Structured Incremental Proof Planning}, booktitle = {{KI-97:} Advances in Artificial Intelligence, 21st Annual German Conference on Artificial Intelligence, Freiburg, Germany, September 9-12, 1997, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {1303}, pages = {63--74}, publisher = {Springer}, year = {1997}, url = {https://doi.org/10.1007/3540634932\_4}, doi = {10.1007/3540634932\_4}, timestamp = {Tue, 14 May 2019 10:00:49 +0200}, biburl = {https://dblp.org/rec/conf/ki/GerberdingP97.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
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.