@inproceedings{0001S19-18,
  title = {Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus},
  author = {Andreas Abel and Christian Sattler},
  year = {2019},
  doi = {10.1145/3354166.3354168},
  url = {https://doi.org/10.1145/3354166.3354168},
  researchr = {https://researchr.org/publication/0001S19-18},
  cites = {0},
  citedby = {0},
  booktitle = {Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019},
  editor = {Ekaterina Komendantskaya},
  publisher = {ACM},
  isbn = {978-1-4503-7249-7},
}

@article{CockxA20,
  title = {Elaborating dependent (co)pattern matching: No pattern left behind},
  author = {Jesper Cockx and Andreas Abel},
  year = {2020},
  doi = {10.1017/S0956796819000182},
  url = {https://doi.org/10.1017/S0956796819000182},
  researchr = {https://researchr.org/publication/CockxA20},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {30},
}

@inproceedings{AbelPTS13,
  title = {Copatterns: programming infinite structures by observations},
  author = {Andreas Abel and Brigitte Pientka and David Thibodeau and Anton Setzer},
  year = {2013},
  doi = {10.1145/2429069.2429075},
  url = {http://doi.acm.org/10.1145/2429069.2429075},
  researchr = {https://researchr.org/publication/AbelPTS13},
  cites = {0},
  citedby = {0},
  pages = {27-38},
  booktitle = {The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013},
  editor = {Roberto Giacobazzi and Radhia Cousot},
  publisher = {ACM},
  isbn = {978-1-4503-1832-7},
}

@article{0001VW17,
  title = {Normalization by evaluation for sized dependent types},
  author = {Andreas Abel and Andrea Vezzosi and Théo Winterhalter},
  year = {2017},
  doi = {10.1145/3110277},
  url = {http://doi.acm.org/10.1145/3110277},
  researchr = {https://researchr.org/publication/0001VW17},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {1},
  number = {ICFP},
}

@article{AbelAS17,
  title = {Interactive programming in Agda - Objects and graphical user interfaces},
  author = {Andreas Abel and Stephan Adelsberger and Anton Setzer},
  year = {2017},
  doi = {10.1017/S0956796816000319},
  url = {http://dx.doi.org/10.1017/S0956796816000319},
  researchr = {https://researchr.org/publication/AbelAS17},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {27},
}

@article{VezzosiM019,
  title = {Cubical agda: a dependently typed programming language with univalence and higher inductive types},
  author = {Andrea Vezzosi and Anders Mörtberg and Andreas Abel},
  year = {2019},
  doi = {10.1145/3341691},
  url = {https://doi.org/10.1145/3341691},
  researchr = {https://researchr.org/publication/VezzosiM019},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
}

@article{AbelAHPMSS19,
  title = {POPLMark reloaded: Mechanizing proofs by logical relations},
  author = {Andreas Abel and Guillaume Allais and Aliya Hameer and Brigitte Pientka and Alberto Momigliano and Steven Schäfer and Kathrin Stark},
  year = {2019},
  doi = {10.1017/S0956796819000170},
  url = {https://doi.org/10.1017/S0956796819000170},
  researchr = {https://researchr.org/publication/AbelAHPMSS19},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {29},
}

@inproceedings{PientkaT00Z19,
  title = {A Type Theory for Defining Logics and Proofs},
  author = {Brigitte Pientka and David Thibodeau and Andreas Abel and Francisco Ferreira 0001 and Rébecca Zucchini},
  year = {2019},
  doi = {10.1109/LICS.2019.8785683},
  url = {https://doi.org/10.1109/LICS.2019.8785683},
  researchr = {https://researchr.org/publication/PientkaT00Z19},
  cites = {0},
  citedby = {0},
  pages = {1-13},
  booktitle = {34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019},
  publisher = {IEEE},
  isbn = {978-1-7281-3608-0},
}

@article{0001OV18,
  title = {Decidability of conversion for type theory in type theory},
  author = {Andreas Abel and Joakim Öhman and Andrea Vezzosi},
  year = {2018},
  doi = {10.1145/3158111},
  url = {http://doi.acm.org/10.1145/3158111},
  researchr = {https://researchr.org/publication/0001OV18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {POPL},
}

@article{0001P16-8,
  title = {Well-founded recursion with copatterns and sized types},
  author = {Andreas Abel and Brigitte Pientka},
  year = {2016},
  doi = {10.1017/S0956796816000022},
  url = {http://dx.doi.org/10.1017/S0956796816000022},
  researchr = {https://researchr.org/publication/0001P16-8},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {26},
}

@inproceedings{000110-2,
  title = {MiniAgda: Integrating Sized and Dependent Types},
  author = {Andreas Abel},
  year = {2010},
  url = {http://www.easychair.org/publications/?page=506004245},
  researchr = {https://researchr.org/publication/000110-2},
  cites = {0},
  citedby = {0},
  pages = {18-32},
  booktitle = {Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010},
  editor = {Ekaterina Komendantskaya and Ana Bove and Milad Niqui},
  volume = {5},
  series = {EPiC Series},
  publisher = {EasyChair},
}

@inproceedings{Setzer0PT14,
  title = {Unnesting of Copatterns},
  author = {Anton Setzer and Andreas Abel and Brigitte Pientka and David Thibodeau},
  year = {2014},
  doi = {10.1007/978-3-319-08918-8_3},
  url = {http://dx.doi.org/10.1007/978-3-319-08918-8_3},
  researchr = {https://researchr.org/publication/Setzer0PT14},
  cites = {0},
  citedby = {0},
  pages = {31-45},
  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},
  editor = {Gilles Dowek},
  volume = {8560},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-319-08917-1},
}

@article{CockxA18,
  title = {Elaborating dependent (co)pattern matching},
  author = {Jesper Cockx and Andreas Abel},
  year = {2018},
  doi = {10.1145/3236770},
  url = {https://doi.org/10.1145/3236770},
  researchr = {https://researchr.org/publication/CockxA18},
  cites = {0},
  citedby = {0},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
}