bibliography.bib

@inproceedings{omar2017hazelnut,
  author = {Omar, Cyrus and Voysey, Ian and Hilton, Michael and Aldrich, Jonathan and Hammer, Matthew A.},
  title = {{Hazelnut: A Bidirectionally Typed Structure Editor Calculus}},
  booktitle = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of Programming Languages (POPL)},
  pages = {86--99},
  publisher = {Association for Computing Machinery},
  year = {2017},
  url = {https://doi.org/10.1145/3009837.3009900},
  doi = {10.1145/3009837.3009900}
}

@inproceedings{omar2019live,
  author = {Omar, Cyrus and Voysey, Ian and Chugh, Ravi and Hammer, Matthew A.},
  title = {{Live Functional Programming with Typed Holes}},
  journal = {Computing Research Repository},
  booktitle = {Proceedings of the 46th {ACM} {SIGPLAN} Symposium on Principles of Programming Languages (POPL)},
  volume = {3},
  pages = {14:1--14:32},
  year = {2019}
}

@book{aho2007compilers,
  title = {{Compilers: Principles, Techniques, and Tools}},
  author = {Aho, Alfred V. and Lam, Monica S. and Sethi, Ravi and Ullman, Jeffrey D.},
  edition = {2nd},
  year = {2007},
  publisher = {Pearson/Addison Wesley}
}

@mastersthesis{ferreira2012compiler,
  title = {{A Compiler for the dependently typed language Beluga}},
  author = {Ferreira Ruiz, Francisco},
  year = {2012},
  school = {Université de Montréal},
  url = {http://hdl.handle.net/1866/8676}
}

@mastersthesis{germain2010implementation,
  title = {{Implementation of a dependently typed functional programming language}},
  author = {Germain, Renaud},
  year = {2010},
  school = {McGill University},
  url = {https://escholarship.mcgill.ca/concern/theses/xd07gt09k}
}

@article{harper1993framework,
  title = {A framework for defining logics},
  author = {Harper, Robert and Honsell, Furio and Plotkin, Gordon},
  journal = {Journal of the ACM (JACM)},
  volume = {40},
  number = {1},
  pages = {143--184},
  year = {1993},
  publisher = {Association for Computing Machinery},
}

@article{pientka2013insider,
  title = {An insider's look at {LF} type reconstruction: everything you (n)ever wanted to know},
  author = {Pientka, Brigitte},
  journal = {Journal of Functional Programming},
  volume = {23},
  number = {1},
  pages = {1--37},
  year = {2013},
  publisher = {Cambridge University Press}
}

@article{thibodeau2021intensional,
  title = {An intensional type theory of coinduction with copatterns},
  author = {Thibodeau, David},
  year = {2021}
}

@inproceedings{ferreira2014bidirectional,
  title = {Bidirectional elaboration of dependently typed programs},
  author = {Ferreira, Francisco and Pientka, Brigitte},
  booktitle = {Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP)},
  pages = {161--174},
  year = {2014}
}

@inproceedings{ferreira2013compiling,
  title = {{Compiling Contextual Objects: Bringing Higher-Order Abstract Syntax to Programmers}},
  author = {Ferreira, Francisco and Monnier, Stefan and Pientka, Brigitte},
  booktitle = {Proceedings of the 7th Workshop on Programming Languages Meets Program Verification (PLPV)},
  pages = {13--24},
  year = {2013}
}

@article{abel2013copatterns,
  title = {Copatterns: Programming infinite structures by observations},
  author = {Abel, Andreas and Pientka, Brigitte and Thibodeau, David and Setzer, Anton},
  journal = {ACM SIGPLAN Notices},
  volume = {48},
  number = {1},
  pages = {27--38},
  year = {2013},
  publisher = {Association for Computing Machinery},
}

@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 of the 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP)},
  series = {{EPTCS}},
  volume = {34},
  pages = {5--20},
  year = {2010},
  url = {https://doi.org/10.4204/EPTCS.34.3},
  doi = {10.4204/EPTCS.34.3}
}

@inproceedings{cave2013first,
  title = {{First-class Substitutions in Contextual Type Theory}},
  author = {Cave, Andrew and Pientka, Brigitte},
  booktitle = {Proceedings of the 8th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP)},
  pages = {15--24},
  year = {2013}
}

@inproceedings{frost2008parser,
  title = {Parser combinators for ambiguous left-recursive grammars},
  author = {Frost, Richard A and Hafiz, Rahmatullah and Callaghan, Paul},
  booktitle = {Proceedings of the 10th Practical Aspects of Declarative Languages: 10th International Symposium, PADL 2008, San Francisco, CA, USA, January 7-8, 2008},
  pages = {167--181},
  year = {2008},
  publisher = {Springer}
}

@inproceedings{danielsson2008parsing,
  title = {{Parsing Mixfix Operators}},
  author = {Danielsson, Nils Anders and Norell, Ulf},
  booktitle = {Proceedings of the 20th International Symposium on the Implementation and Application of Functional Languages (IFL)},
  pages = {80--99},
  year = {2008},
  publisher = {Springer}
}

@article{dijkstra1961algol,
  title = {{Algol 60 Translation: An Algol 60 Translator for the X1 and Making a Translator for Algol 60}},
  author = {Dijkstra, Edsger Wybe},
  journal = {Stichting Mathematisch Centrum. Rekenafdeling},
  number = {MR 34/61},
  year = {1961},
  publisher = {Stichting Mathematisch Centrum}
}

@phdthesis{afroozeh2019practical,
  title = {{Practical General Top-down Parsers}},
  author = {Afroozeh, Ali and Izmaylova, Anastasia},
  year = {2019},
  school = {University of Amsterdam}
}

@article{ferreira2018proofs,
  author = {Francisco Ferreira Ruiz},
  title = {Proofs and Programs about Open Terms},
  journal = {Computing Research Repository},
  volume = {abs/1805.07176},
  year = {2018},
  url = {http://arxiv.org/abs/1805.07176},
  eprinttype = {arXiv},
  eprint = {1805.07176}
}

@inproceedings{jim2010semantics,
  title = {Semantics and algorithms for data-dependent grammars},
  author = {Jim, Trevor and Mandelbaum, Yitzhak and Walker, David},
  booktitle = {Proceedings of the 37th {ACM} {SIGPLAN} Symposium on Principles of Programming Languages (POPL)},
  pages = {417--430},
  year = {2010}
}

@article{mens2004survey,
  title = {A survey of software refactoring},
  author = {Mens, Tom and Tourwé, Tom},
  journal = {IEEE Transactions on software engineering},
  volume = {30},
  number = {2},
  pages = {126--139},
  year = {2004},
  publisher = {IEEE}
}

@article{teitelbaum1981cornell,
  title = {The {Cornell} program synthesizer: a syntax-directed programming environment},
  author = {Teitelbaum, Tim and Reps, Thomas},
  journal = {Communications of the ACM},
  volume = {24},
  number = {9},
  pages = {563--573},
  year = {1981},
  publisher = {Association for Computing Machinery},
}

@inproceedings{pientka2010beluga,
  title = {Beluga: A framework for programming and reasoning with deductive systems (system description)},
  author = {Pientka, Brigitte and Dunfield, Jana},
  booktitle = {Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR)},
  pages = {15--21},
  year = {2010},
  publisher = {Springer}
}

@article{nanevski2008contextual,
  title = {{Contextual Modal Type Theory}},
  author = {Nanevski, Aleksandar and Pfenning, Frank and Pientka, Brigitte},
  journal = {ACM Transactions on Computational Logic (TOCL)},
  volume = {9},
  number = {3},
  pages = {1--49},
  year = {2008},
  publisher = {Association for Computing Machinery},
}

@inproceedings{clffolp,
  author = {Abel, Andreas and Coquand, Thierry and Norell, Ulf},
  editor = {Gramlich, Bernhard},
  title = {{Connecting a Logical Framework to a First-Order Logic Prover}},
  booktitle = {Frontiers of Combining Systems},
  year = {2005},
  publisher = {Springer Berlin Heidelberg},
  address = {Berlin, Heidelberg},
  pages = {285--301},
  isbn = {978-3-540-31730-2}
}

@misc{Coq,
  title = {{The Coq Proof Assistant Reference Manual}},
  author = {The Coq Development Team},
  note = {Version 8.18.0},
  year = {2023},
  howpublished = {\url{http://coq.inria.fr}}
}

@book{bertot2013interactive,
  title = {Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions},
  author = {Bertot, Yves and Castéran, Pierre},
  year = {2013},
  publisher = {Springer Science \& Business Media}
}

@inproceedings{errington2021harpoon,
  title = {{Harpoon: Mechanizing Metatheory Interactively: (System Description)}},
  author = {Errington, Jacob and Jang, Junyoung and Pientka, Brigitte},
  booktitle = {Proceedings of the 28th International Conference on Automated Deduction (CADE)},
  pages = {636--648},
  year = {2021},
  publisher = {Springer}
}

@book{nipkow2002isabelle,
  title = {Isabelle/HOL: a proof assistant for higher-order logic},
  author = {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},
  series = {LNCS},
  volume = {2283},
  year = {2002},
  publisher = {Springer Science \& Business Media}
}

@misc{wenzel2023isabelleimpl,
  title = {The {Isabelle/Isar} Implementation},
  author = {Wenzel, Makarius and Berghofer, Stefan and Haftmann, Florian and Paulson, Larry},
  year = {2023},
  howpublished = {\url{https://isabelle.in.tum.de/doc/implementation.pdf}}
}

@misc{wenzel2023isabelleisarref,
  title = {The {Isabelle/Isar} Reference Manual},
  author = {Wenzel, Makarius and Ballarin, Clemens and Berghofer, Stefan and Blanchette, Jasmin and Bourke, Timothy and Bulwahn, Lukas and  Chaieb, Amine and Dixon, Lucas and Haftmann, Florian and Huffman, Brian and Hupel, Lars and Klein, Gerwin and Krauss, Alexander and Kunčar, Ondřej and Lochbihler, Andreas and Nipkow, Tobias and Noschinski, Lars and von Oheimb, David and Paulson, Larry and Skalberg, Sebastian and Sternagel, Christian and Traytel, Dmitriy},
  year = {2023},
  howpublished = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}
}

@misc{wenzel2023isabellesys,
  title = {The {Isabelle} System Manual},
  author = {Wenzel, Makarius},
  year = {2023},
  howpublished = {\url{https://isabelle.in.tum.de/doc/system.pdf}}
}

@inproceedings{ballarin2006interpretation,
  title = {{Interpretation of locales in Isabelle: Theories and proof contexts}},
  author = {Ballarin, Clemens},
  booktitle = {Proceedings of the 5th International Conference on Mathematical Knowledge Management (MKM)},
  pages = {31--43},
  year = {2006},
  publisher = {Springer}
}

@inproceedings{lean4,
  author = {Moura, Leonardo de and Ullrich, Sebastian},
  editor = {Platzer, André and Sutcliffe, Geoff},
  title = {The Lean 4 Theorem Prover and Programming Language},
  booktitle = {Proceedings of the 28th International Conference on Automated Deduction (CADE)},
  year = {2021},
  publisher = {Springer},
  address = {Cham},
  pages = {625--635},
  isbn = {978-3-030-79876-5}
}

@techreport{hutton1996monadic,
  author = {Graham Hutton and Erik Meijer},
  title = {Monadic Parser Combinators},
  institution = {Department of Computer Science, University of Nottingham},
  type = {Technical Report},
  number = {NOTTCS-TR-96-4},
  year = {1996}
}

@inproceedings{generalparsercombs,
  author = {Izmaylova, Anastasia and Afroozeh, Ali and Storm, Tijs van der},
  title = {Practical, General Parser Combinators},
  year = {2016},
  isbn = {9781450340977},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/2847538.2847539},
  doi = {10.1145/2847538.2847539},
  booktitle = {Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM)},
  pages = {1–12},
  numpages = {12},
  keywords = {higher-order functions, general parsing, left recursion, memoization, Parser combinators, continuation-passing style},
  location = {St. Petersburg, FL, USA}
}

@techreport{leijen2001parsec,
  author = {Leijen, Daan and Meijer, Erik},
  title = {{Parsec: Direct Style Monadic Parser Combinators for the Real World}},
  year = {2001},
  url = {https://www.microsoft.com/en-us/research/publication/parsec-direct-style-monadic-parser-combinators-for-the-real-world/},
  edition = {Technical Report UU-CS-2001-35, Departement of Computer Science, Universiteit Utrecht},
  institution = {Universiteit Utrecht},
  number = {UU-CS-2001-27}
}

@book{Burge1975-BURRPT,
  year = {1975},
  author = {William H. Burge},
  publisher = {Addison-Wesley},
  title = {Recursive Programming Techniques}
}

@article{oppen1980prettyprinting,
  title = {Prettyprinting},
  author = {Oppen, Dereck C},
  journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume = {2},
  number = {4},
  pages = {465--483},
  year = {1980},
  publisher = {Association for Computing Machinery},
}

@misc{leroy2022ocaml,
  title = {{The OCaml system release 5.0: Documentation and user's manual}},
  author = {Leroy, Xavier and Doligez, Damien and Frisch, Alain and Garrigue, Jacques and Rémy, Didier and Vouillon, Jérôme},
  year = {2022},
  school = {Inria}
}

@misc{de2003camlp4,
  title = {Camlp4 reference manual},
  author = {de Rauglaudre, Daniel},
  journal = {Online (September 2003)},
  year = {2003},
  note = {Version 3.07},
  howpublished = {\url{https://caml.inria.fr/pub/docs/manual-camlp4/index.html}}
}

@inproceedings{pfenning1988higher,
  author = {Pfenning, F. and Elliott, C.},
  title = {{Higher-Order Abstract Syntax}},
  year = {1988},
  issn = {0362-1340},
  publisher = {Association for Computing Machinery},
  url = {https://doi.org/10.1145/53990.54010},
  doi = {10.1145/53990.54010},
  booktitle = {Proceedings of the {ACM} SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI)},
  pages = {199–208},
  numpages = {10}
}

@article{chomsky1956three,
  title = {Three models for the description of language},
  author = {Chomsky, Noam},
  journal = {IRE Transactions on information theory},
  volume = {2},
  number = {3},
  pages = {113--124},
  year = {1956},
  publisher = {IEEE}
}

@article{unambiguousprec,
  title = {Characterizing unambiguous precedence systems in expressions without superfluous parentheses},
  author = {Wafik Boulos Lotfallah},
  journal = {International Journal of Computer Mathematics},
  volume = {86},
  number = {1},
  pages = {1-20},
  year  = {2009},
  publisher = {Taylor & Francis},
  doi = {10.1080/00207160802166499},
  url = {https://doi.org/10.1080/00207160802166499},
  eprint = {https://doi.org/10.1080/00207160802166499}
}

@article{najd2016trees,
  title = {Trees that grow},
  author = {Najd, Shayan and Jones, Simon Peyton},
  journal = {arXiv preprint arXiv:1610.04799},
  year = {2016}
}

@inbook{barendregt2003,
  author = {Barendregt, Henk},
  editor = {Kamareddine, Fairouz D.},
  title = {Towards an Interactive Mathematical Proof Mode},
  bookTitle = {Thirty Five Years of Automating Mathematics},
  year = {2003},
  publisher = {Springer Netherlands},
  address = {Dordrecht},
  pages = {25--36},
  isbn = {978-94-017-0253-9},
  doi = {10.1007/978-94-017-0253-9_2},
  url = {https://doi.org/10.1007/978-94-017-0253-9_2}
}

@article{kaiser2018,
  author = {Kaiser, Jan-Oliver and Ziliani, Beta and Krebbers, Robbert and R\'{e}gis-Gianas, Yann and Dreyer, Derek},
  title = {Mtac2: Typed Tactics for Backward Reasoning in Coq},
  year = {2018},
  issue_date = {September 2018},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {2},
  number = {ICFP},
  url = {https://doi.org/10.1145/3236773},
  doi = {10.1145/3236773},
  journal = {Proceedings of the ACM on Programming Languages},
  articleno = {78},
  numpages = {31},
  keywords = {Theorem Proving, Coq, Dependent Types, Metaprogramming, Tactic Languages}
}

@inproceedings{delahaye2000tactic,
  title = {A tactic language for the system {Coq}},
  author = {Delahaye, David},
  booktitle = {Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR)},
  pages = {85--95},
  year = {2000},
  publisher = {Springer}
}

@article{smith2007ocamllex,
  title = {{OCamllex} and {OCamlyacc}},
  author = {Smith, Joshua B.},
  journal = {Practical OCaml},
  pages = {193--211},
  year = {2007},
  publisher = {Springer}
}

@article{foundation2008pientka,
  author = {Pientka, Brigitte},
  title = {{A Type-Theoretic Foundation for Programming with Higher-Order Abstract Syntax and First-Class Substitutions}},
  year = {2008},
  issue_date = {January 2008},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  journal = {35th {ACM} {SIGPLAN} Symposium on Principles of Programming Languages (POPL)},
  pages = {371--382}
}

@incollection{pientka2010programming,
  title = {Programming inductive proofs: A new approach based on contextual types},
  author = {Pientka, Brigitte},
  booktitle = {Verification, Induction, Termination Analysis},
  pages = {1--16},
  year = {2010},
  publisher = {Springer}
}

@article{resolveAmbiguity,
  author = {Viktor Palmkvist and Elias Castegren and Philipp Haller and David Broman},
  title = {Resolvable Ambiguity},
  journal = {Computing Research Repository},
  volume = {abs/1911.05672},
  year = {2019},
  url = {http://arxiv.org/abs/1911.05672},
  eprinttype = {arXiv},
  eprint = {1911.05672},
  timestamp = {Mon, 02 Dec 2019 13:44:01 +0100},
  biburl = {https://dblp.org/rec/journals/corr/abs-1911-05672.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{baelde2014abella,
  title = {Abella: A system for reasoning about relational specifications},
  author = {Baelde, David and Chaudhuri, Kaustuv and Gacek, Andrew and Miller, Dale and Nadathur, Gopalan and Tiu, Alwen and Wang, Yuting},
  journal = {Journal of Formalized Reasoning},
  volume = {7},
  number = {2},
  pages = {1--89},
  year = {2014}
}

@article{DEBRUIJN1972381,
  title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
  journal = {Indagationes Mathematicae (Proceedings)},
  volume = {75},
  number = {5},
  pages = {381-392},
  year = {1972},
  issn = {1385-7258},
  doi = {https://doi.org/10.1016/1385-7258(72)90034-0},
  url = {https://www.sciencedirect.com/science/article/pii/1385725872900340},
  author = {Nicolaas Govert {de Bruijn}},
}

@inproceedings{debruijnlevels1995,
  author = {Lescanne, Pierre and Rouyer-Degli, Jocelyne},
  year = {1995},
  pages = {294-308},
  title = {{Explicit Substitutions with de Bruijn's Levels}},
  series = {LNCS},
  volume = {914},
  isbn = {978-3-540-59200-6},
  doi = {10.1007/3-540-59200-8_65}
}

@phdthesis{norell2007towards,
  title = {Towards a practical programming language based on dependent type theory},
  author = {Norell, Ulf},
  year = {2007},
  school = {Chalmers University of Technology}
}

@software{agda2023,
  author = {{Agda Team}},
  title = {Agda 2.6.4},
  year = {2023},
  note = {\url{https://wiki.portal.chalmers.se/agda/pmwiki.php}},
}

@inproceedings{creager_et_al:OASIcs.EVCS.2023.8,
  author = {Creager, Douglas A. and van Antwerpen, Hendrik},
  title = {{Stack Graphs: Name Resolution at Scale}},
  booktitle = {Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages = {8:1--8:12},
  series = {Open Access Series in Informatics (OASIcs)},
  ISBN = {978-3-95977-267-9},
  ISSN = {2190-6807},
  year = {2023},
  volume = {109},
  editor = {L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2023/17778},
  URN = {urn:nbn:de:0030-drops-177789},
  doi = {10.4230/OASIcs.EVCS.2023.8},
  annote = {Keywords: Scope graphs, name binding, code navigation}
}

@inproceedings{vanantwerpen_et_al:LIPIcs.ECOOP.2021.1,
  author = {van Antwerpen, Hendrik and Visser, Eelco},
  title = {{Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers}},
  booktitle = {Proceedings of the 35th European Conference on Object-Oriented Programming (ECOOP)},
  pages = {1:1--1:29},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN = {978-3-95977-190-0},
  ISSN = {1868-8969},
  year = {2021},
  volume = {194},
  editor = {M{\o}ller, Anders and Sridharan, Manu},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.1},
  URN = {urn:nbn:de:0030-drops-140441},
  doi = {10.4230/LIPIcs.ECOOP.2021.1},
  annote = {Keywords: type checking, name resolution, parallel algorithms}
}

@inproceedings{nameresolution,
  author = {Neron, Pierre and Tolmach, Andrew  and Visser, Eelco and Wachsmuth, Guido},
  title = {{A Theory of Name Resolution}},
  booktitle = {Proceedings of the 24th European Symposium on Programming Languages and Systems (ESOP)},
  year = {2015},
  publisher = {Springer},
  pages = {205--231},
  isbn = {978-3-662-46669-8}
}

@article{poplmarkreloaded,
  title = {{POPLMark reloaded: Mechanizing proofs by logical relations}},
  volume = {29},
  DOI = {10.1017/S0956796819000170},
  journal = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  author = {Abel, Andreas and Allais, Guillaume and Hameer, Aliya and Pientka, Brigitte and Momigliano, Alberto and Schäfer, Steven and Stark, Kathrin},
  year = {2019},
  pages = {e19}
}

@inproceedings{sano2023,
  author = {Sano, Chuta and Kavanagh, Ryan and Pientka, Brigitte},
  title = {{Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity}},
  year = {2023},
  issue_date = {October 2023},
  publisher = {Association for Computing Machinery},
  volume = {7},
  url = {https://doi.org/10.1145/3622810},
  doi = {10.1145/3622810},
  booktitle = {Proceedings of the {ACM} {SIGPLAN} on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA)},
  articleno = {235},
  numpages = {26}
}

@InProceedings{inductivebeluga,
  author = {Pientka, Brigitte and Cave, Andrew},
  title = {{Inductive Beluga: Programming Proofs}},
  booktitle = {Proceedings of the 25th International Conference on Automated Deduction (CADE)},
  year = {2015},
  publisher = {Springer},
  pages = {272–281}
}

@inproceedings{dunfield2009,
  author = {Dunfield, Jana and Pientka, Brigitte},
  title = {{Case Analysis of Higher-Order Data}},
  year = {2009},
  booktitle = {Proceedings of the 3rd International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP)},
  publisher = {Elsevier Science Publishers B. V.},
  volume = {228},
  url = {https://doi.org/10.1016/j.entcs.2008.12.117},
  doi = {10.1016/j.entcs.2008.12.117},
  journal = {Electronic Notes in Theoretical Computer Science},
  pages = {69--84},
  numpages = {16}
}

@inproceedings{felty2010reasoning,
  author = {Felty, Amy and Pientka, Brigitte},
  title = {{Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison}},
  booktitle = {Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP)},
  pages = {227--242},
  year = {2010},
  publisher = {Springer}
}

@inproceedings{Twelf,
  author = {Pfenning, Frank and Sch{\"u}rmann, Carsten},
  title = {{System Description: Twelf --- A Meta-Logical Framework for Deductive Systems}},
  booktitle = {{Proceedings of the 16th International Conference on Automated Deduction (CADE)}},
  year = {1999},
  publisher = {Springer},
  pages = {202--206}
}