@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 = {ppdp},
}

@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 = {JFP},
  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 = {POPL},
}

@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 = {PACMPL},
  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 = {JFP},
  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 = {PACMPL},
  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 = {JFP},
  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 = {lics},
}

@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 = {PACMPL},
  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 = {JFP},
  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 = {itp},
}

@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 = {RTA},
}

@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 = {PACMPL},
  volume = {2},
  number = {ICFP},
}