1. Eliminating dependent pattern matching without K. (30th August 2016) Authors: COCKX, JESPER; DEVRIESE, DOMINIQUE; PIESSENS, FRANK Journal: Journal of functional programming Issue: Volume 26(2016) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗
2. Leibniz equality is isomorphic to Martin-Löf identity, parametrically. (17th June 2020) Authors: ABEL, ANDREAS; COCKX, JESPER; DEVRIESE, DOMINIQUE; TIMANY, AMIN; WADLER, PHILIP Journal: Journal of functional programming Issue: Volume 30(2020) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗
3. Linear capabilities for fully abstract compilation of separation-logic-verified code. (30th March 2021) Authors: VAN STRYDONCK, THOMAS; PIESSENS, FRANK; DEVRIESE, DOMINIQUE Journal: Journal of functional programming Issue: Volume 31(2021) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗
4. Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory. (10th May 2018) Authors: COCKX, JESPER; DEVRIESE, DOMINIQUE Journal: Journal of functional programming Issue: Volume 28(2018) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗
5. StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. (15th April 2021) Authors: SKORSTENGAARD, LAU; DEVRIESE, DOMINIQUE; BIRKEDAL, LARS Journal: Journal of functional programming Issue: Volume 31(2021) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗