Overlapping and Order-Independent Patterns - Definitional Equality for All. - Jesper Cockx; Frank Piessens; Dominique Devriese (ESOP, 2014)

Pattern matching without K. - Jesper Cockx; Dominique Devriese; Frank Piessens (ICFP, 2014)

Unifiers as equivalences: proof-relevant unification of dependently typed data. - Jesper Cockx; Dominique Devriese; Frank Piessens (ICFP, 2016)

Eliminating dependent pattern matching without K. - Jesper Cockx; Dominique Devriese; Frank Piessens (J. Funct. Program., 2016)

Lifting proof-relevant unification to higher dimensions. - Jesper Cockx; Dominique Devriese (CPP, 2017)

Expressive and strongly type-safe code generation. - Thomas Winant; Jesper Cockx; Dominique Devriese (PPDP, 2017)

Dependent Pattern Matching and Proof-Relevant Unification. - Jesper Cockx (2017)

Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory. - Jesper Cockx; Dominique Devriese (J. Funct. Program., 2018)

Elaborating dependent (co)pattern matching. - Jesper Cockx; Andreas Abel 001 (Proc. ACM Program. Lang., 2018)

Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. - Jesper Cockx (TYPES, 2019)

Definitional proof-irrelevance without K. - Gaëtan Gilbert; Jesper Cockx; Matthieu Sozeau; Nicolas Tabareau (Proc. ACM Program. Lang., 2019)

Leibniz equality is isomorphic to Martin-Löf identity, parametrically. - Andreas Abel 001; Jesper Cockx; Dominique Devriese; Amin Timany; Philip Wadler (J. Funct. Program., 2020)

Elaborating dependent (co)pattern matching: No pattern left behind. - Jesper Cockx; Andreas Abel 001 (J. Funct. Program., 2020)

Extracting the power of dependent types. - Artjoms Sinkarovs; Jesper Cockx (GPCE, 2021)

Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection. - Artjoms Sinkarovs; Jesper Cockx (CoRR, 2021)

The taming of the rew: a type theory with computational assumptions. - Jesper Cockx; Nicolas Tabareau; Théo Winterhalter (Proc. ACM Program. Lang., 2021)

Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs. - Jesper Cockx; Orestis Melkonian; Lucas Escot; James Chapman 001; Ulf Norell (Haskell, 2022)

Optimising First-Class Pattern Matching. - Jeff Smits; Toine Hartman; Jesper Cockx (SLE, 2022)

Practical generic programming over a universe of native datatypes. - Lucas Escot; Jesper Cockx (Proc. ACM Program. Lang., 2022)

Dependently Typed Languages in Statix. - Jonathan Brouwer; Jesper Cockx; Aron Zwaan (Eelco Visser Commemorative Symposium, 2023)

ExEl: Building an Elaborator Using Extensible Constraints. - Bohdan Liesnikov; Jesper Cockx (IFL, 2023)

Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. - Bohdan Liesnikov; Jesper Cockx (APLAS, 2024)

Pinpointing the Learning Obstacles of an Interactive Theorem Prover. - Sára Juhosová; Andy Zaidman; Jesper Cockx (ICPC, 2025)