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: "Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019"
  editor:
  - name: "Ekaterina Komendantskaya"
    link: "https://researchr.org/alias/ekaterina-komendantskaya"
  publisher: "ACM"
  isbn: "978-1-4503-7249-7"
  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: "Journal of Functional Programming"
  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: "The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013"
  editor:
  - name: "Roberto Giacobazzi"
    link: "https://researchr.org/alias/roberto-giacobazzi"
  - name: "Radhia Cousot"
    link: "https://researchr.org/alias/radhia-cousot"
  publisher: "ACM"
  isbn: "978-1-4503-1832-7"
  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: "Proceedings of the ACM on Programming Languages"
  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: "Journal of Functional Programming"
  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: "Proceedings of the ACM on Programming Languages"
  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: "Journal of Functional Programming"
  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: "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"
  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: "Proceedings of the ACM on Programming Languages"
  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: "Journal of Functional Programming"
  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: "Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010"
  editor:
  - name: "Ekaterina Komendantskaya"
    link: "https://researchr.org/alias/ekaterina-komendantskaya"
  - name: "Ana Bove"
    link: "https://researchr.org/alias/ana-bove"
  - name: "Milad Niqui"
    link: "https://researchr.org/alias/milad-niqui"
  volume: "5"
  series: "EPiC Series"
  publisher: "EasyChair"
  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: "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:
  - name: "Gilles Dowek"
    link: "https://researchr.org/alias/gilles-dowek"
  volume: "8560"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-08917-1"
  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: "Proceedings of the ACM on Programming Languages"
  volume: "2"
  number: "ICFP"
  kind: "article"
  key: "CockxA18"