Jesper Cockx

According to our database, Jesper Cockx authored at least 22 papers between 2014 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language.

Bohdan Liesnikov, Jesper Cockx

Proceedings of the Programming Languages and Systems - 22nd Asian Symposium, 2024

2023

ExEl: Building an Elaborator Using Extensible Constraints.

Bohdan Liesnikov, Jesper Cockx

Proceedings of the 35th Symposium on Implementation and Application of Functional Languages, 2023

Dependently Typed Languages in Statix.

Jonathan Brouwer, Jesper Cockx, Aron Zwaan

Proceedings of the Eelco Visser Commemorative Symposium, 2023

2022

Practical generic programming over a universe of native datatypes.

Lucas Escot, Jesper Cockx

Proc. ACM Program. Lang., 2022

Optimising First-Class Pattern Matching.

Jeff Smits, Toine Hartman, Jesper Cockx

Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, 2022

Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs.

Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, Ulf Norell

Proceedings of the Haskell '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15, 2022

2021

The taming of the rew: a type theory with computational assumptions.

Jesper Cockx, Nicolas Tabareau, Théo Winterhalter

Proc. ACM Program. Lang., 2021

Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection.

Artjoms Sinkarovs, Jesper Cockx

CoRR, 2021

Extracting the power of dependent types.

Artjoms Sinkarovs, Jesper Cockx

Proceedings of the GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17, 2021

2020

Elaborating dependent (co)pattern matching: No pattern left behind.

Jesper Cockx, Andreas Abel

J. Funct. Program., 2020

Leibniz equality is isomorphic to Martin-Löf identity, parametrically.

Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler

J. Funct. Program., 2020

2019

Definitional proof-irrelevance without K.

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau

Proc. ACM Program. Lang., 2019

Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules.

Jesper Cockx

Proceedings of the 25th International Conference on Types for Proofs and Programs, 2019

2018

Elaborating dependent (co)pattern matching.

Jesper Cockx, Andreas Abel

Proc. ACM Program. Lang., 2018

Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory.

Jesper Cockx, Dominique Devriese

J. Funct. Program., 2018

2017

Dependent Pattern Matching and Proof-Relevant Unification.

Jesper Cockx

PhD thesis, 2017

Expressive and strongly type-safe code generation.

Thomas Winant, Jesper Cockx, Dominique Devriese

Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09, 2017

Lifting proof-relevant unification to higher dimensions.

Jesper Cockx, Dominique Devriese

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Eliminating dependent pattern matching without K.

Jesper Cockx, Dominique Devriese, Frank Piessens

J. Funct. Program., 2016

Unifiers as equivalences: proof-relevant unification of dependently typed data.

Jesper Cockx, Dominique Devriese, Frank Piessens

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2014

Pattern matching without K.

Jesper Cockx, Dominique Devriese, Frank Piessens

Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

Overlapping and Order-Independent Patterns - Definitional Equality for All.

Jesper Cockx, Frank Piessens, Dominique Devriese

Proceedings of the Programming Languages and Systems, 2014