StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details. - Lau Skorstengaard; Dominique Devriese; Lars Birkedal (CoRR, 2018)

Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details. - Lau Skorstengaard; Dominique Devriese; Lars Birkedal (CoRR, 2019)

An Introduction to Logical Relations. - Lau Skorstengaard (CoRR, 2019)

StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. - Lau Skorstengaard; Dominique Devriese; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. - Lau Skorstengaard; Dominique Devriese; Lars Birkedal (ACM Trans. Program. Lang. Syst., 2020)