publications:
- title: "Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Christian Sattler"
    link: "https://researchr.org/alias/christian-sattler"
  year: "2019"
  doi: "https://doi.org/10.1145/3354166.3354168"
  links:
    doi: "https://doi.org/10.1145/3354166.3354168"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/0001S19"
  researchr: "https://researchr.org/publication/0001S19-18"
  cites: 0
  citedby: 0
  booktitle: "ppdp"
  kind: "inproceedings"
  key: "0001S19-18"
- title: "Elaborating dependent (co)pattern matching: No pattern left behind"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  year: "2020"
  doi: "https://doi.org/10.1017/S0956796819000182"
  links:
    doi: "https://doi.org/10.1017/S0956796819000182"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/CockxA20"
  researchr: "https://researchr.org/publication/CockxA20"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "30"
  kind: "article"
  key: "CockxA20"
- title: "Copatterns: programming infinite structures by observations"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  - name: "David Thibodeau"
    link: "https://researchr.org/alias/david-thibodeau"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2429069.2429075"
  links:
    doi: "http://doi.acm.org/10.1145/2429069.2429075"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/AbelPTS13"
  researchr: "https://researchr.org/publication/AbelPTS13"
  cites: 0
  citedby: 0
  pages: "27-38"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "AbelPTS13"
- title: "Normalization by evaluation for sized dependent types"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  - name: "Théo Winterhalter"
    link: "https://researchr.org/alias/th%C3%A9o-winterhalter"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3110277"
  links:
    doi: "http://doi.acm.org/10.1145/3110277"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/0001VW17"
  researchr: "https://researchr.org/publication/0001VW17"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "1"
  number: "ICFP"
  kind: "article"
  key: "0001VW17"
- title: "Interactive programming in Agda - Objects and graphical user interfaces"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Stephan Adelsberger"
    link: "https://researchr.org/alias/stephan-adelsberger"
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  year: "2017"
  doi: "http://dx.doi.org/10.1017/S0956796816000319"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000319"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AbelAS17"
  researchr: "https://researchr.org/publication/AbelAS17"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "27"
  kind: "article"
  key: "AbelAS17"
- title: "Cubical agda: a dependently typed programming language with univalence and higher inductive types"
  author:
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  - name: "Anders Mörtberg"
    link: "https://researchr.org/alias/anders-m%C3%B6rtberg"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  year: "2019"
  doi: "https://doi.org/10.1145/3341691"
  links:
    doi: "https://doi.org/10.1145/3341691"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/VezzosiM019"
  researchr: "https://researchr.org/publication/VezzosiM019"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  number: "ICFP"
  kind: "article"
  key: "VezzosiM019"
- title: "POPLMark reloaded: Mechanizing proofs by logical relations"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  - name: "Aliya Hameer"
    link: "https://researchr.org/alias/aliya-hameer"
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  - name: "Alberto Momigliano"
    link: "https://researchr.org/alias/alberto-momigliano"
  - name: "Steven Schäfer"
    link: "https://researchr.org/alias/steven-sch%C3%A4fer"
  - name: "Kathrin Stark"
    link: "https://researchr.org/alias/kathrin-stark"
  year: "2019"
  doi: "https://doi.org/10.1017/S0956796819000170"
  links:
    doi: "https://doi.org/10.1017/S0956796819000170"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AbelAHPMSS19"
  researchr: "https://researchr.org/publication/AbelAHPMSS19"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "29"
  kind: "article"
  key: "AbelAHPMSS19"
- title: "A Type Theory for Defining Logics and Proofs"
  author:
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  - name: "David Thibodeau"
    link: "https://researchr.org/alias/david-thibodeau"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Francisco Ferreira 0001"
    link: "https://researchr.org/alias/francisco-ferreira-0001"
  - name: "Rébecca Zucchini"
    link: "https://researchr.org/alias/r%C3%A9becca-zucchini"
  year: "2019"
  doi: "https://doi.org/10.1109/LICS.2019.8785683"
  links:
    doi: "https://doi.org/10.1109/LICS.2019.8785683"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/PientkaT00Z19"
  researchr: "https://researchr.org/publication/PientkaT00Z19"
  cites: 0
  citedby: 0
  pages: "1-13"
  booktitle: "lics"
  kind: "inproceedings"
  key: "PientkaT00Z19"
- title: "Decidability of conversion for type theory in type theory"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Joakim Öhman"
    link: "https://researchr.org/alias/joakim-%C3%B6hman"
  - name: "Andrea Vezzosi"
    link: "https://researchr.org/alias/andrea-vezzosi"
  year: "2018"
  doi: "http://doi.acm.org/10.1145/3158111"
  links:
    doi: "http://doi.acm.org/10.1145/3158111"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/0001OV18"
  researchr: "https://researchr.org/publication/0001OV18"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "2"
  number: "POPL"
  kind: "article"
  key: "0001OV18"
- title: "Well-founded recursion with copatterns and sized types"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  year: "2016"
  doi: "http://dx.doi.org/10.1017/S0956796816000022"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000022"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/0001P16"
  researchr: "https://researchr.org/publication/0001P16-8"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "26"
  kind: "article"
  key: "0001P16-8"
- title: "MiniAgda: Integrating Sized and Dependent Types"
  author:
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  year: "2010"
  doi: "http://www.easychair.org/publications/?page=506004245"
  links:
    doi: "http://www.easychair.org/publications/?page=506004245"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/000110"
  researchr: "https://researchr.org/publication/000110-2"
  cites: 0
  citedby: 0
  pages: "18-32"
  booktitle: "itp"
  kind: "inproceedings"
  key: "000110-2"
- title: "Unnesting of Copatterns"
  author:
  - name: "Anton Setzer"
    link: "https://researchr.org/alias/anton-setzer"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  - name: "Brigitte Pientka"
    link: "https://researchr.org/alias/brigitte-pientka"
  - name: "David Thibodeau"
    link: "https://researchr.org/alias/david-thibodeau"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-08918-8_3"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-08918-8_3"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/rta/Setzer0PT14"
  researchr: "https://researchr.org/publication/Setzer0PT14"
  cites: 0
  citedby: 0
  pages: "31-45"
  booktitle: "RTA"
  kind: "inproceedings"
  key: "Setzer0PT14"
- title: "Elaborating dependent (co)pattern matching"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Andreas Abel"
    link: "http://www.cse.chalmers.se/~abela/"
  year: "2018"
  doi: "https://doi.org/10.1145/3236770"
  links:
    doi: "https://doi.org/10.1145/3236770"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/CockxA18"
  researchr: "https://researchr.org/publication/CockxA18"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "2"
  number: "ICFP"
  kind: "article"
  key: "CockxA18"