2 citations · 3 across the 3 of their papers we have counts for
3 papers
Context-Dependent Effects and Concurrency in Guarded Interaction Trees
Sergei Stepanenko, Emma Nardino, Virgil Marionneau +3
Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Rocq. We present an extension of…
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
We propose a calling convention for capability machines with local capabilities. The calling convention ensures local-state encapsulation and well-bracketed control flow. We use th…
StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
We propose and study StkTokens: a new calling convention that provably enforces well-bracketed control flow and local state encapsulation on a capability machine. The calling conve…