| 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 | 83 | 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 | 36 | 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 | 18 | 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 |
| 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 | 6 | 2022 |
| Elaborating dependent (co) pattern matching: No pattern left behind J Cockx, A Abel Journal of Functional Programming 30, e2, 2020 | 6 | 2020 |
| 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 | 5 | 2022 |
| 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 |
| 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 | 2 | 2021 |
Dominique DevrieseKU LeuvenAdresse e-mail validée de kuleuven.be
