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
692019
Pattern matching without K
J Cockx, D Devriese, F Piessens
Proceedings of the 19th ACM SIGPLAN international conference on Functional …, 2014
492014
Sprinkles of extensionality for your vanilla type theory
J Cockx, A Abel
Abstract of a talk at TYPES, 2016
332016
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
292021
Elaborating dependent (co) pattern matching
J Cockx, A Abel
Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018
242018
The agda wiki
U Norell, NA Danielsson, A Abel, J Cockx
212005
Dependent pattern matching and proof-relevant unification
J Cockx
192017
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
Type theory unchained: Extending agda with user-defined rewrite rules
J Cockx
25th International Conference on Types for Proofs and Programs (TYPES 2019), 2020
142020
Eliminating dependent pattern matching without K
J Cockx, D Devriese, F Piessens
Journal of functional programming 26, e16, 2016
142016
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
122018
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
102014
Lifting proof-relevant unification to higher dimensions
J Cockx, D Devriese
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017
82017
Elaborating dependent (co) pattern matching: No pattern left behind
J Cockx, A Abel
Journal of Functional Programming 30, e2, 2020
42020
Overlapping and order-independent patterns in type theory
J Cockx
Master thesis, KU Leuven, 2013
42013
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
32022
How to tame your rewrite rules
J Cockx, N Tabareau, T Winterhalter
Types for Proofs and Programs, TYPES, 2019
32019
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
22020
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
22020
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
The system can't perform the operation now. Try again later.
Articles 1–20