My publications

Papers and abstracts

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).

Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, and Philip Wadler. February 2018. Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically. Submitted to the Journal of Functional Programming (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.

Talks

March 2018. Elaborating dependent (co)pattern matching. Talk at the 2nd Göteborg-Stockholm Type Theory Seminar in Stockholm (slides).

September 2017. Depending on equations: A proof-relevant framework for unification in dependent type theory. Invited talk at the 31st International Workshop on Unification in Oxford (slides).

April 2016. A sound unification algorithm based on telescope equivalences. Talk at the 23rd Agda Meeting in Glasgow (slides).

September 2015. STAMP: Strongly Type-sAfe Meta-Programming. Talk at the 22nd Agda Meeting in Leuven (slides).

June 2015. Unification in a context of postponed equations. Talk at the 21st Agda Meeting in Göteborg (slides).

May 2014. Eliminating dependent pattern matching without K. Talk at the 19nd Agda Meeting in Paris.