Follow
Jesper Cockx
Title
Cited by
Cited by
Year
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
512019
Pattern matching without K
J Cockx, D Devriese, F Piessens
Proceedings of the 19th ACM SIGPLAN international conference on Functional …, 2014
432014
Sprinkles of extensionality for your vanilla type theory
J Cockx, A Abel
Abstract of a talk at TYPES, 2016
312016
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
202021
Elaborating dependent (co) pattern matching
J Cockx, A Abel
Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018
202018
The agda wiki
U Norell, NA Danielsson, A Abel, J Cockx
202005
Unifiers as equivalences: Proof-relevant unification of dependently typed data
J Cockx, D Devriese, F Piessens
Acm Sigplan Notices 51 (9), 270-283, 2016
192016
Dependent pattern matching and proof-relevant unification
J Cockx
162017
Eliminating dependent pattern matching without K
J Cockx, D Devriese, F Piessens
Journal of functional programming 26, 2016
112016
Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory
J Cockx, D Devriese
Journal of Functional Programming 28, 2018
82018
Lifting proof-relevant unification to higher dimensions
J Cockx, D Devriese
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017
82017
Overlapping and order-independent patterns
J Cockx, F Piessens, D Devriese
European Symposium on Programming Languages and Systems, 87-106, 2014
82014
Type theory unchained: Extending Agda with user-defined rewrite rules
J Cockx
25th International Conference on Types for Proofs and Programs (TYPES 2019), 2020
72020
Overlapping and order-independent patterns in type theory
J Cockx
Ph. D. thesis, Master thesis, KU Leuven, 2013
32013
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
22020
How to tame your rewrite rules
J Cockx, N Tabareau, T Winterhalter
Types for Proofs and Programs, TYPES, 2019
22019
Expressive and strongly type-safe code generation
T Winant, J Cockx, D Devriese
Proceedings of the 19th International Symposium on Principles and Practice …, 2017
22017
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
12021
Elaborating dependent (co) pattern matching: No pattern left behind
J Cockx, A Abel
Journal of Functional Programming 30, 2020
12020
Vectors are records, too
J Cockx, G Gilbert, N Tabareau
TYPES 2018, 2018
12018
The system can't perform the operation now. Try again later.
Articles 1–20