@article{EscotC22,
  title = {Practical generic programming over a universe of native datatypes},
  author = {Lucas Escot and Jesper Cockx},
  year = {2022},
  doi = {10.1145/3547644},
  url = {https://doi.org/10.1145/3547644},
  researchr = {https://researchr.org/publication/EscotC22},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {6},
  number = {ICFP},
  pages = {625-649},
}

@inproceedings{CockxPD14,
  title = {Overlapping and Order-Independent Patterns - Definitional Equality for All},
  author = {Jesper Cockx and Frank Piessens and Dominique Devriese},
  year = {2014},
  doi = {10.1007/978-3-642-54833-8_6},
  url = {http://dx.doi.org/10.1007/978-3-642-54833-8_6},
  researchr = {https://researchr.org/publication/CockxPD14},
  cites = {0},
  citedby = {0},
  pages = {87-106},
  booktitle = {ESOP},
}

@article{GilbertCST19,
  title = {Definitional proof-irrelevance without K},
  author = {Gaëtan Gilbert and Jesper Cockx and Matthieu Sozeau and Nicolas Tabareau},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290316},
  researchr = {https://researchr.org/publication/GilbertCST19},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {3},
}

@inproceedings{Cockx19,
  title = {Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules},
  author = {Jesper Cockx},
  year = {2019},
  doi = {10.4230/LIPIcs.TYPES.2019.2},
  url = {https://doi.org/10.4230/LIPIcs.TYPES.2019.2},
  researchr = {https://researchr.org/publication/Cockx19},
  cites = {0},
  citedby = {0},
  booktitle = {TYPES},
}

@inproceedings{WinantCD17,
  title = {Expressive and strongly type-safe code generation},
  author = {Thomas Winant and Jesper Cockx and Dominique Devriese},
  year = {2017},
  doi = {10.1145/3131851.3131872},
  url = {http://doi.acm.org/10.1145/3131851.3131872},
  researchr = {https://researchr.org/publication/WinantCD17},
  cites = {0},
  citedby = {0},
  pages = {199-210},
  booktitle = {ppdp},
}

@inproceedings{CockxME0N22,
  title = {Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs},
  author = {Jesper Cockx and Orestis Melkonian and Lucas Escot and James Chapman and Ulf Norell},
  year = {2022},
  doi = {10.1145/3546189.3549920},
  url = {https://doi.org/10.1145/3546189.3549920},
  researchr = {https://researchr.org/publication/CockxME0N22},
  cites = {0},
  citedby = {0},
  pages = {108-122},
  booktitle = {haskell},
}

@inproceedings{CockxDP16,
  title = {Unifiers as equivalences: proof-relevant unification of dependently typed data},
  author = {Jesper Cockx and Dominique Devriese and Frank Piessens},
  year = {2016},
  doi = {10.1145/2951913.2951917},
  url = {http://doi.acm.org/10.1145/2951913.2951917},
  researchr = {https://researchr.org/publication/CockxDP16},
  cites = {0},
  citedby = {0},
  pages = {270-283},
  booktitle = {ICFP},
}

@phdthesis{basesearch-7836,
  title = {Dependent Pattern Matching and Proof-Relevant Unification},
  author = {Jesper Cockx},
  year = {2017},
  url = {https://www.base-search.net/Record/66a7ce9719c00dd2b976ac2c0f472c9fa527c0fcc5fbe259b2c5ca71b4f5ecc7},
  note = {base-search.net (ftunivleuven:oai:lirias.kuleuven.be:123456789/583556)},
  researchr = {https://researchr.org/publication/basesearch-7836},
  cites = {0},
  citedby = {0},
  school = {Katholieke Universiteit Leuven, Belgium},
}

@inproceedings{CockxD17,
  title = {Lifting proof-relevant unification to higher dimensions},
  author = {Jesper Cockx and Dominique Devriese},
  year = {2017},
  doi = {10.1145/3018610.3018612},
  url = {http://doi.acm.org/10.1145/3018610.3018612},
  researchr = {https://researchr.org/publication/CockxD17},
  cites = {0},
  citedby = {0},
  pages = {173-181},
  booktitle = {CPP},
}

@inproceedings{SmitsHC22,
  title = {Optimising First-Class Pattern Matching},
  author = {Jeff Smits and Toine Hartman and Jesper Cockx},
  year = {2022},
  doi = {10.1145/3567512.3567519},
  url = {https://doi.org/10.1145/3567512.3567519},
  researchr = {https://researchr.org/publication/SmitsHC22},
  cites = {0},
  citedby = {0},
  pages = {74-83},
  booktitle = {SLE},
}

@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},
}

@article{CockxDP16-0,
  title = {Eliminating dependent pattern matching without K},
  author = {Jesper Cockx and Dominique Devriese and Frank Piessens},
  year = {2016},
  doi = {10.1017/S0956796816000174},
  url = {http://dx.doi.org/10.1017/S0956796816000174},
  researchr = {https://researchr.org/publication/CockxDP16-0},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {26},
}

@article{AbelCDTW20,
  title = {Leibniz equality is isomorphic to Martin-Löf identity, parametrically},
  author = {Andreas Abel 0001 and Jesper Cockx and Dominique Devriese and Amin Timany and Philip Wadler},
  year = {2020},
  doi = {10.1017/S0956796820000155},
  url = {https://doi.org/10.1017/S0956796820000155},
  researchr = {https://researchr.org/publication/AbelCDTW20},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {30},
}

@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{CockxDP14,
  title = {Pattern matching without K},
  author = {Jesper Cockx and Dominique Devriese and Frank Piessens},
  year = {2014},
  doi = {10.1145/2628136.2628139},
  url = {http://doi.acm.org/10.1145/2628136.2628139},
  researchr = {https://researchr.org/publication/CockxDP14},
  cites = {0},
  citedby = {0},
  pages = {257-268},
  booktitle = {ICFP},
}

@article{CockxD18,
  title = {Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory},
  author = {Jesper Cockx and Dominique Devriese},
  year = {2018},
  doi = {10.1017/S095679681800014X},
  url = {https://doi.org/10.1017/S095679681800014X},
  researchr = {https://researchr.org/publication/CockxD18},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {28},
}

@article{CockxTW21,
  title = {The taming of the rew: a type theory with computational assumptions},
  author = {Jesper Cockx and Nicolas Tabareau and Théo Winterhalter},
  year = {2021},
  doi = {10.1145/3434341},
  url = {https://doi.org/10.1145/3434341},
  researchr = {https://researchr.org/publication/CockxTW21},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {5},
  number = {POPL},
  pages = {1-29},
}

@inproceedings{BrouwerCZ23,
  title = {Dependently Typed Languages in Statix},
  author = {Jonathan Brouwer and Jesper Cockx and Aron Zwaan},
  year = {2023},
  doi = {10.4230/OASIcs.EVCS.2023.6},
  url = {https://doi.org/10.4230/OASIcs.EVCS.2023.6},
  researchr = {https://researchr.org/publication/BrouwerCZ23},
  cites = {0},
  citedby = {0},
  booktitle = {BIRTHDAY},
}

@inproceedings{SinkarovsC21,
  title = {Extracting the power of dependent types},
  author = {Artjoms Sinkarovs and Jesper Cockx},
  year = {2021},
  doi = {10.1145/3486609.3487201},
  url = {https://doi.org/10.1145/3486609.3487201},
  researchr = {https://researchr.org/publication/SinkarovsC21},
  cites = {0},
  citedby = {0},
  pages = {83-95},
  booktitle = {GPCE},
}