Definitional proof-irrelevance without K G Gilbert, J Cockx, M Sozeau, N Tabareau Proceedings of the ACM on Programming Languages 3 (POPL), 1-28, 2019 | 84 | 2019 |

Pattern matching without K J Cockx, D Devriese, F Piessens Proceedings of the 19th ACM SIGPLAN international conference on Functional …, 2014 | 53 | 2014 |

The taming of the rew: a type theory with computational assumptions J Cockx, N Tabareau, T Winterhalter Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021 | 37 | 2021 |

Sprinkles of extensionality for your vanilla type theory A Abel, J Cockx 22nd International Conference on Types for Proofs and Programs, TYPES 2016, 2016 | 34 | 2016 |

Dependent pattern matching and proof-relevant unification J Cockx | 24 | 2017 |

Elaborating dependent (co) pattern matching J Cockx, A Abel Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018 | 22 | 2018 |

Unifiers as equivalences: Proof-relevant unification of dependently typed data J Cockx, D Devriese, F Piessens Acm Sigplan Notices 51 (9), 270-283, 2016 | 21 | 2016 |

The agda wiki U Norell, NA Danielsson, A Abel, J Cockx | 21 | 2005 |

Type theory unchained: Extending agda with user-defined rewrite rules J Cockx 25th International Conference on Types for Proofs and Programs, TYPES 2019, 2, 2020 | 19 | 2020 |

Eliminating dependent pattern matching without K J Cockx, D Devriese, F Piessens Journal of functional programming 26, e16, 2016 | 14 | 2016 |

Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory J Cockx, D Devriese Journal of Functional Programming 28, e12, 2018 | 12 | 2018 |

Overlapping and Order-Independent Patterns: Definitional Equality for All J Cockx, F Piessens, D Devriese Programming Languages and Systems: 23rd European Symposium on Programming …, 2014 | 10 | 2014 |

Lifting proof-relevant unification to higher dimensions J Cockx, D Devriese Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 9 | 2017 |

Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs J Cockx, O Melkonian, L Escot, J Chapman, U Norell Proceedings of the 15th ACM SIGPLAN International Haskell Symposium, 108-122, 2022 | 8 | 2022 |

Practical generic programming over a universe of native datatypes L Escot, J Cockx Proceedings of the ACM on Programming Languages 6 (ICFP), 625-649, 2022 | 7 | 2022 |

Elaborating dependent (co) pattern matching: No pattern left behind J Cockx, A Abel Journal of Functional Programming 30, e2, 2020 | 6 | 2020 |

Leibniz equality is isomorphic to Martin-Löf identity, parametrically A Abel, J Cockx, D Devriese, A Timany, P Wadler Journal of Functional Programming 30, e17, 2020 | 4 | 2020 |

How to tame your rewrite rules J Cockx, N Tabareau, T Winterhalter Types for Proofs and Programs, TYPES, 2019 | 4 | 2019 |

Overlapping and order-independent patterns in type theory J Cockx Master thesis, KU Leuven, 2013 | 4 | 2013 |

Extracting the power of dependent types A Šinkarovs, J Cockx Proceedings of the 20th ACM SIGPLAN International Conference on Generative …, 2021 | 2 | 2021 |