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
602019
Pattern matching without K
J Cockx, D Devriese, F Piessens
Proceedings of the 19th ACM SIGPLAN international conference on Functional …, 2014
472014
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
222021
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
122016
Type theory unchained: Extending Agda with user-defined rewrite rules
J Cockx
25th International Conference on Types for Proofs and Programs (TYPES 2019), 2020
102020
Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory
J Cockx, D Devriese
Journal of Functional Programming 28, 2018
92018
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
Elaborating dependent (co) pattern matching: No pattern left behind
J Cockx, A Abel
Journal of Functional Programming 30, 2020
32020
Overlapping and order-independent patterns in type theory
J Cockx
Ph. D. thesis, Master thesis, KU Leuven, 2013
32013
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, 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
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
12022
The system can't perform the operation now. Try again later.
Articles 1–20