My publications

Bohdan Liesnikov and Jesper Cockx. October 2024. Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. At the 2024 Asian Symposium on Programming Languages and Systems, APLAS 2024 (PDF).

Kayleigh Lieverse, Lucas Escot, and Jesper Cockx. June 2024. A Generic Translation from Case Trees to Eliminators. At the 30nd International Conference on Types for Proofs and Programs, TYPES 2024 (PDF).

Bohdan Liesnikov, and Jesper Cockx. February 2024. ExEl: Building an elaborator using extensible constraints. In the IFL '23 post-proceedings (PDF).

Ivar de Bruin, Bohdan Liesnikov, and Jesper Cockx. September 2023. Improving Agda's Module System. Presented at IFL '23 (PDF).

Jesper Cockx. June 2023. Operations on Syntax Should Not Inspect Their Scope. At the 29nd International Conference on Types for Proofs and Programs, TYPES 2023 (PDF) (slides).

Bohdan Liesnikov and Jesper Cockx. June 2023. Building an elaborator using extensible constraints. At the 29nd International Conference on Types for Proofs and Programs, TYPES 2023 (PDF).

Jonathan Brouwer, Jesper Cockx, and Aaron Zwaan. April 2023. Dependently Typed Languages in Statix. At the Eelco Visser Commemorative Symposium, EVCS (PDF).

Jeff Smits, Toine Hartman, and Jesper Cockx. December 2022. Optimising First-Class Pattern Matching. At the 15nd International Conference on Software Language Engineering, SLE 2022 (PDF).

Lucas Escot and Jesper Cockx. September 2022. Practical Generic Programming Over a Universe Of Native Datatypes. In the Proceedings of the ACM on Programming Languages, ICFP 2022 (PDF).

Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, and Ulf Norell. September 2022. Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs. At the 15nd International Haskell Symposium, Haskell 2022 (PDF).

Artjoms Šinkarovs and Jesper Cockx. October 2021. Extracting The Power of Dependent Types. GPCE 2021 (PDF).

Jesper Cockx, Nicolas Tabareau, Théo Winterhalter. January 2021. The Taming of the Rew: A Type Theory with Computational Assumptions. In the Proceedings of the ACM on Programming Languages, POPL 2021 (PDF).

Jesper Cockx. September 2020. Type theory unchained: Extending type theory with user-defined rewrite rules. TYPES 2019 post-proceedings (LIPIcs volume 175) (PDF).

Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, and Philip Wadler. June 2020. Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically. Journal of Functional Programming (PDF).

Jesper Cockx and Andreas Abel. January 2020. Elaborating dependent (co)pattern matching: no pattern left behind. In the Journal of Functional Programming, JFP 30.

Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. June 2019. Modular Confluence for Rewrite Rules in MetaCoq. At the 26nd International Conference on Types for Proofs and Programs, TYPES 2020 (cancelled due to COVID-19) (PDF).

Jesper Cockx, Théo Winterhalter, and Nicolas Tabareau. June 2019. How to tame your rewrite rules. At the 25nd International Conference on Types for Proofs and Programs, TYPES 2019 (PDF) (slides).

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. January 2019. Definitional proof-irrelevance without K. In the Proceedings of the ACM on Programming Languages, POPL 2019 (PDF).

Jesper Cockx and Andreas Abel. September 2018. Elaborating dependent (co)pattern matching. At the ACM SIGPLAN International Conference on Functional Programming, ICFP 2018 (PDF).

Jesper Cockx, Gaetan Gilbert, and Nicolas Tabareau. June 2018. Vectors are Records, too. At the 24nd International Conference on Types for Proofs and Programs, TYPES 2018 (PDF) (slides).

Jesper Cockx and Dominique Devriese. May 2018. Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory. In the Journal of Functional Programming, JFP 28 (PDF).

Thomas Winant, Jesper Cockx, and Dominique Devriese. October 2017. Expressive and Strongly Type-Safe Code Generation. At the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP '17.

Jesper Cockx, Dominique Devriese (advisor), Frank Piessens (advisor). June 2017. Dependent Pattern Matching and Proof-Relevant Unification. PhD thesis, KU Leuven (PDF) (slides).

Thomas Winant, Jesper Cockx, and Dominique Devriese. May 2017. Expressive and Strongly Type-Safe Code Generation. At the 23nd International Conference on Types for Proofs and Programs, TYPES 2017 (PDF).

Jesper Cockx and Dominique Devriese. January 2017. Lifting proof-relevant unification to higher dimensions. At the 6th Conference on Certified Programs and Proofs, CPP 2017 (PDF) (slides).

Jesper Cockx, Dominique Devriese, and Frank Piessens. September 2016. Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data. At the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016 (PDF) (slides).

Jesper Cockx and Dominique Devriese. August 2016. Eliminating Dependent Pattern Matching Without K. In the Journal of Functional Programming, JFP 26.

Jesper Cockx and Andreas Abel. May 2016. Sprinkles of Extensionality for Your Vanilla Type Theory. At the 22nd International Conference on Types for Proofs and Programs, TYPES 2016 (PDF) (slides).

Andreas Nuyts, Jesper Cockx, Dominique Devriese, and Frank Piessens. June 2015. Towards a directed HoTT with four kinds of variance. At the Workshop on Homotopy Type Theory / Univalent Foundations, HoTT/UF 2015.

Jesper Cockx, Dominique Devriese, and Frank Piessens. September 2014. Pattern matching without K. At the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014 (PDF) (slides).

Jesper Cockx, Dominique Devriese, and Frank Piessens. April 2014. Overlapping and Order-Independent Patterns: Definitional Equality for All. At the 23rd European Symposium on Programming, ESOP 2014 (PDF).

Jesper Cockx, Dominique Devriese (advisor), Frank Piessens (advisor). June 2013. Overlapping and Order-Independent Patterns in Type Theory. Master thesis, KU Leuven.