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 | 68 | 2019 |

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

Sprinkles of extensionality for your vanilla type theory J Cockx, A Abel Abstract of a talk at TYPES, 2016 | 32 | 2016 |

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 | 28 | 2021 |

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

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

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

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

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

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

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 | 8 | 2017 |

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

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

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 | 3 | 2022 |

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

25th International Conference on Types for Proofs and Programs (TYPES 2019) M Kohlhase, F Rabe, M Wenzel, J Cockx, S Alves, D Kesner, D Ventura, ... Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2020 | 2 | 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 | 2 | 2020 |

Expressive and strongly type-safe code generation T Winant, J Cockx, D Devriese Proceedings of the 19th International Symposium on Principles and Practice …, 2017 | 2 | 2017 |