publications:
- title: "Practical generic programming over a universe of native datatypes"
  author:
  - name: "Lucas Escot"
    link: "https://researchr.org/alias/lucas-escot"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2022"
  doi: "https://doi.org/10.1145/3547644"
  links:
    doi: "https://doi.org/10.1145/3547644"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/EscotC22"
  researchr: "https://researchr.org/publication/EscotC22"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "6"
  number: "ICFP"
  pages: "625-649"
  kind: "article"
  key: "EscotC22"
- title: "Overlapping and Order-Independent Patterns - Definitional Equality for All"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-642-54833-8_6"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-54833-8_6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/CockxPD14"
  researchr: "https://researchr.org/publication/CockxPD14"
  cites: 0
  citedby: 0
  pages: "87-106"
  booktitle: "ESOP"
  kind: "inproceedings"
  key: "CockxPD14"
- title: "Definitional proof-irrelevance without K"
  author:
  - name: "Gaëtan Gilbert"
    link: "https://researchr.org/alias/ga%C3%ABtan-gilbert"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Matthieu Sozeau"
    link: "https://researchr.org/alias/matthieu-sozeau"
  - name: "Nicolas Tabareau"
    link: "https://researchr.org/alias/nicolas-tabareau"
  year: "2019"
  doi: "https://dl.acm.org/citation.cfm?id=3290316"
  links:
    doi: "https://dl.acm.org/citation.cfm?id=3290316"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/GilbertCST19"
  researchr: "https://researchr.org/publication/GilbertCST19"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "3"
  kind: "article"
  key: "GilbertCST19"
- title: "Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2019"
  doi: "https://doi.org/10.4230/LIPIcs.TYPES.2019.2"
  links:
    doi: "https://doi.org/10.4230/LIPIcs.TYPES.2019.2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/types/Cockx19"
  researchr: "https://researchr.org/publication/Cockx19"
  cites: 0
  citedby: 0
  booktitle: "TYPES"
  kind: "inproceedings"
  key: "Cockx19"
- title: "Expressive and strongly type-safe code generation"
  author:
  - name: "Thomas Winant"
    link: "https://researchr.org/alias/thomas-winant"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3131851.3131872"
  links:
    doi: "http://doi.acm.org/10.1145/3131851.3131872"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/WinantCD17"
  researchr: "https://researchr.org/publication/WinantCD17"
  cites: 0
  citedby: 0
  pages: "199-210"
  booktitle: "ppdp"
  kind: "inproceedings"
  key: "WinantCD17"
- title: "Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Orestis Melkonian"
    link: "https://researchr.org/alias/orestis-melkonian"
  - name: "Lucas Escot"
    link: "https://researchr.org/alias/lucas-escot"
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Ulf Norell"
    link: "https://researchr.org/alias/ulf-norell"
  year: "2022"
  doi: "https://doi.org/10.1145/3546189.3549920"
  links:
    doi: "https://doi.org/10.1145/3546189.3549920"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/CockxME0N22"
  researchr: "https://researchr.org/publication/CockxME0N22"
  cites: 0
  citedby: 0
  pages: "108-122"
  booktitle: "haskell"
  kind: "inproceedings"
  key: "CockxME0N22"
- title: "Unifiers as equivalences: proof-relevant unification of dependently typed data"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2951913.2951917"
  links:
    doi: "http://doi.acm.org/10.1145/2951913.2951917"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/CockxDP16"
  researchr: "https://researchr.org/publication/CockxDP16"
  cites: 0
  citedby: 0
  pages: "270-283"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "CockxDP16"
- title: "Dependent Pattern Matching and Proof-Relevant Unification"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2017"
  doi: "https://www.base-search.net/Record/66a7ce9719c00dd2b976ac2c0f472c9fa527c0fcc5fbe259b2c5ca71b4f5ecc7"
  links:
    doi: "https://www.base-search.net/Record/66a7ce9719c00dd2b976ac2c0f472c9fa527c0fcc5fbe259b2c5ca71b4f5ecc7"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/basesearch/Cockx17"
  researchr: "https://researchr.org/publication/basesearch-7836"
  cites: 0
  citedby: 0
  school: "Katholieke Universiteit Leuven, Belgium"
  kind: "phdthesis"
  key: "basesearch-7836"
- title: "Lifting proof-relevant unification to higher dimensions"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2017"
  doi: "http://doi.acm.org/10.1145/3018610.3018612"
  links:
    doi: "http://doi.acm.org/10.1145/3018610.3018612"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/CockxD17"
  researchr: "https://researchr.org/publication/CockxD17"
  cites: 0
  citedby: 0
  pages: "173-181"
  booktitle: "CPP"
  kind: "inproceedings"
  key: "CockxD17"
- title: "Optimising First-Class Pattern Matching"
  author:
  - name: "Jeff Smits"
    link: "https://www.jeffsmits.net/"
  - name: "Toine Hartman"
    link: "https://www.linkedin.com/in/toinehartman/"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2022"
  doi: "https://doi.org/10.1145/3567512.3567519"
  links:
    doi: "https://doi.org/10.1145/3567512.3567519"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sle/SmitsHC22"
  researchr: "https://researchr.org/publication/SmitsHC22"
  cites: 0
  citedby: 0
  pages: "74-83"
  booktitle: "SLE"
  kind: "inproceedings"
  key: "SmitsHC22"
- 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"
- title: "Eliminating dependent pattern matching without K"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2016"
  doi: "http://dx.doi.org/10.1017/S0956796816000174"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796816000174"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/CockxDP16"
  researchr: "https://researchr.org/publication/CockxDP16-0"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "26"
  kind: "article"
  key: "CockxDP16-0"
- title: "Leibniz equality is isomorphic to Martin-Löf identity, parametrically"
  author:
  - name: "Andreas Abel 0001"
    link: "https://researchr.org/alias/andreas-abel-0001"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Amin Timany"
    link: "https://researchr.org/alias/amin-timany"
  - name: "Philip Wadler"
    link: "https://researchr.org/alias/philip-wadler"
  year: "2020"
  doi: "https://doi.org/10.1017/S0956796820000155"
  links:
    doi: "https://doi.org/10.1017/S0956796820000155"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AbelCDTW20"
  researchr: "https://researchr.org/publication/AbelCDTW20"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "30"
  kind: "article"
  key: "AbelCDTW20"
- 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: "Pattern matching without K"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  - name: "Frank Piessens"
    link: "https://researchr.org/alias/frank-piessens"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2628136.2628139"
  links:
    doi: "http://doi.acm.org/10.1145/2628136.2628139"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/CockxDP14"
  researchr: "https://researchr.org/publication/CockxDP14"
  cites: 0
  citedby: 0
  pages: "257-268"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "CockxDP14"
- title: "Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Dominique Devriese"
    link: "https://researchr.org/alias/dominique-devriese"
  year: "2018"
  doi: "https://doi.org/10.1017/S095679681800014X"
  links:
    doi: "https://doi.org/10.1017/S095679681800014X"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/CockxD18"
  researchr: "https://researchr.org/publication/CockxD18"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "28"
  kind: "article"
  key: "CockxD18"
- title: "The taming of the rew: a type theory with computational assumptions"
  author:
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Nicolas Tabareau"
    link: "https://researchr.org/alias/nicolas-tabareau"
  - name: "Théo Winterhalter"
    link: "https://researchr.org/alias/th%C3%A9o-winterhalter"
  year: "2021"
  doi: "https://doi.org/10.1145/3434341"
  links:
    doi: "https://doi.org/10.1145/3434341"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/CockxTW21"
  researchr: "https://researchr.org/publication/CockxTW21"
  cites: 0
  citedby: 0
  journal: "PACMPL"
  volume: "5"
  number: "POPL"
  pages: "1-29"
  kind: "article"
  key: "CockxTW21"
- title: "Dependently Typed Languages in Statix"
  author:
  - name: "Jonathan Brouwer"
    link: "https://researchr.org/alias/jonathan-brouwer"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  - name: "Aron Zwaan"
    link: "https://aronzwaan.github.io"
  year: "2023"
  doi: "https://doi.org/10.4230/OASIcs.EVCS.2023.6"
  links:
    doi: "https://doi.org/10.4230/OASIcs.EVCS.2023.6"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/birthday/BrouwerCZ23"
  researchr: "https://researchr.org/publication/BrouwerCZ23"
  cites: 0
  citedby: 0
  booktitle: "BIRTHDAY"
  kind: "inproceedings"
  key: "BrouwerCZ23"
- title: "Extracting the power of dependent types"
  author:
  - name: "Artjoms Sinkarovs"
    link: "https://researchr.org/alias/artjoms-sinkarovs"
  - name: "Jesper Cockx"
    link: "https://jesper.sikanda.be"
  year: "2021"
  doi: "https://doi.org/10.1145/3486609.3487201"
  links:
    doi: "https://doi.org/10.1145/3486609.3487201"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/gpce/SinkarovsC21"
  researchr: "https://researchr.org/publication/SinkarovsC21"
  cites: 0
  citedby: 0
  pages: "83-95"
  booktitle: "GPCE"
  kind: "inproceedings"
  key: "SinkarovsC21"