Jesper Cockx - RankMe

25 papers A 4B 4C 2Journal 9Unranked 3

Year	Rank	Type	Title / Venue / Authors
2025	A	`conf`	Pinpointing the Learning Obstacles of an Interactive Theorem Prover. ICPC Sára Juhosová, Andy Zaidman, Jesper Cockx
2024	B	`conf`	Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. APLAS Bohdan Liesnikov, Jesper Cockx
2024	—	`ed.`	Proceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe 2024, Milan, Italy, 6 September 2024 TyDe@ICFP Sandra Alves, Jesper Cockx
2023	—	`conf`	Dependently Typed Languages in Statix. Eelco Visser Commemorative Symposium Jonathan Brouwer, Jesper Cockx, Aron Zwaan
2023	—	`conf`	ExEl: Building an Elaborator Using Extensible Constraints. IFL Bohdan Liesnikov, Jesper Cockx
2022	—	`ed.`	27th International Conference on Types for Proofs and Programs, TYPES 2021, Leiden, The Netherlands (Virtual Conference), June 14-18, 2021 TYPES Henning Basold, Jesper Cockx, Silvia Ghilezan
2022	B	`conf`	Optimising First-Class Pattern Matching. SLE Jeff Smits, Toine Hartman, Jesper Cockx
2022	J	`jnl`	Practical generic programming over a universe of native datatypes. Proc. ACM Program. Lang. Lucas Escot, Jesper Cockx
2022	C	`conf`	Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs. Haskell Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, Ulf Norell
2021	J	`jnl`	Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection. CoRR Artjoms Sinkarovs, Jesper Cockx
2021	B	`conf`	Extracting the power of dependent types. GPCE Artjoms Sinkarovs, Jesper Cockx
2021	J	`jnl`	The taming of the rew: a type theory with computational assumptions. Proc. ACM Program. Lang. Jesper Cockx, Nicolas Tabareau, Théo Winterhalter
2020	J	`jnl`	Elaborating dependent (co)pattern matching: No pattern left behind. J. Funct. Program. Jesper Cockx, Andreas Abel
2020	J	`jnl`	Leibniz equality is isomorphic to Martin-Löf identity, parametrically. J. Funct. Program. Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler
2019	J	`jnl`	Definitional proof-irrelevance without K. Proc. ACM Program. Lang. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
2019	—	`conf`	Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. TYPES Jesper Cockx
2018	J	`jnl`	Elaborating dependent (co)pattern matching. Proc. ACM Program. Lang. Jesper Cockx, Andreas Abel
2018	J	`jnl`	Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory. J. Funct. Program. Jesper Cockx, Dominique Devriese
2017	—	`—`	Dependent Pattern Matching and Proof-Relevant Unification. Jesper Cockx
2017	C	`conf`	Expressive and strongly type-safe code generation. PPDP Thomas Winant, Jesper Cockx, Dominique Devriese
2017	B	`conf`	Lifting proof-relevant unification to higher dimensions. CPP Jesper Cockx, Dominique Devriese
2016	J	`jnl`	Eliminating dependent pattern matching without K. J. Funct. Program. Jesper Cockx, Dominique Devriese, Frank Piessens
2016	A	`conf`	Unifiers as equivalences: proof-relevant unification of dependently typed data. ICFP Jesper Cockx, Dominique Devriese, Frank Piessens
2014	A	`conf`	Overlapping and Order-Independent Patterns - Definitional Equality for All. ESOP Jesper Cockx, Frank Piessens, Dominique Devriese
2014	A	`conf`	Pattern matching without K. ICFP Jesper Cockx, Dominique Devriese, Frank Piessens