| 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 | 51 | 2019 |
| Pattern matching without K J Cockx, D Devriese, F Piessens Proceedings of the 19th ACM SIGPLAN international conference on Functional …, 2014 | 43 | 2014 |
| Sprinkles of extensionality for your vanilla type theory J Cockx, A Abel Abstract of a talk at TYPES, 2016 | 31 | 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 | 20 | 2021 |
| Elaborating dependent (co) pattern matching J Cockx, A Abel Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018 | 20 | 2018 |
| The agda wiki U Norell, NA Danielsson, A Abel, J Cockx | 20 | 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 | 16 | 2017 |
| Eliminating dependent pattern matching without K J Cockx, D Devriese, F Piessens Journal of functional programming 26, 2016 | 11 | 2016 |
| Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory J Cockx, D Devriese Journal of Functional Programming 28, 2018 | 8 | 2018 |
| 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 |
| Overlapping and order-independent patterns J Cockx, F Piessens, D Devriese European Symposium on Programming Languages and Systems, 87-106, 2014 | 8 | 2014 |
| Type theory unchained: Extending Agda with user-defined rewrite rules J Cockx 25th International Conference on Types for Proofs and Programs (TYPES 2019), 2020 | 7 | 2020 |
| Overlapping and order-independent patterns in type theory J Cockx Ph. D. thesis, Master thesis, KU Leuven, 2013 | 3 | 2013 |
| 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, 2020 | 2 | 2020 |
| How to tame your rewrite rules J Cockx, N Tabareau, T Winterhalter Types for Proofs and Programs, TYPES, 2019 | 2 | 2019 |
| 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 |
| Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection A Šinkarovs, J Cockx arXiv preprint arXiv:2105.10819, 2021 | 1 | 2021 |
| Elaborating dependent (co) pattern matching: No pattern left behind J Cockx, A Abel Journal of Functional Programming 30, 2020 | 1 | 2020 |
| Vectors are records, too J Cockx, G Gilbert, N Tabareau TYPES 2018, 2018 | 1 | 2018 |
Dominique DevrieseKU LeuvenVerified email at kuleuven.be
