BibTeX records: Brigitte Pientka

download as .bib file

@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}
}
a service of  Schloss Dagstuhl - Leibniz Center for Informatics