StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities (Q5016212): Difference between revisions

Latest revision as of 09:34, 30 July 2024

scientific article; zbMATH DE number 7443767

Language	Label	Description	Also known as
English	StkTokens<i>: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities</i>	scientific article; zbMATH DE number 7443767

Statements

instance of

scholarly article

0 references

title

StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities (English)

0 references

0 references

0 references

0 references

Journal of Functional Programming

0 references

publication date

13 December 2021

0 references

full work available at URL

https://arxiv.org/abs/1811.02787

0 references

MaRDI profile type

MaRDI publication profile

0 references

cites work

An equivalence-preserving CPS translation via multi-language semantics

0 references

Solving reflexive domain equations in a category of complete metric spaces

0 references

A verified information-flow architecture

0 references

Step-indexed kripke models over recursive worlds

0 references

Programming semantics for multiprogrammed computations

0 references

Q4596778

0 references

Iris from the ground up: A modular foundation for higher-order concurrent separation logic

0 references

Game semantics and linear CPS interpretation

0 references

Fully abstract compilation via universal embedding

0 references

Fully-abstract compilation by approximate back-translation

0 references

Data Types as Lattices

0 references

Reasoning about a machine with local capabilities. Provably safe stack and return pointer management

0 references

StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

0 references

A kripke logical relation for effect-based program transformations

0 references

Linear capabilities for fully abstract compilation of separation-logic-verified code

0 references

Identifiers

DOI

10.1017/S095679682100006X

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:5016212

@@ Property / author @@
-Lars Birkedal
@@ Property / author: Lars Birkedal / rank @@
-Normal rank
@@ Property / author @@
+Lars Birkedal
@@ Property / author: Lars Birkedal / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+An equivalence-preserving CPS translation via multi-language semantics
+Normal rank
@@ Property / cites work @@
+Solving reflexive domain equations in a category of complete metric spaces
+Normal rank
@@ Property / cites work @@
+A verified information-flow architecture
@@ Property / cites work: A verified information-flow architecture / rank @@
+Normal rank
@@ Property / cites work @@
+Step-indexed kripke models over recursive worlds
@@ Property / cites work: Step-indexed kripke models over recursive worlds / rank @@
+Normal rank
@@ Property / cites work @@
+Programming semantics for multiprogrammed computations
+Normal rank
@@ Property / cites work @@
+Q4596778
@@ Property / cites work: Q4596778 / rank @@
+Normal rank
@@ Property / cites work @@
+Iris from the ground up: A modular foundation for higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+Game semantics and linear CPS interpretation
@@ Property / cites work: Game semantics and linear CPS interpretation / rank @@
+Normal rank
@@ Property / cites work @@
+Fully abstract compilation via universal embedding
+Normal rank
@@ Property / cites work @@
+Fully-abstract compilation by approximate back-translation
+Normal rank
@@ Property / cites work @@
+Data Types as Lattices
@@ Property / cites work: Data Types as Lattices / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
+Normal rank
@@ Property / cites work @@
+StkTokens<i>: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities</i>
+Normal rank
@@ Property / cites work @@
+A kripke logical relation for effect-based program transformations
+Normal rank
@@ Property / cites work @@
+Linear capabilities for fully abstract compilation of separation-logic-verified code
+Normal rank
@@ Property / OpenAlex ID @@
+W3152835471
@@ Property / OpenAlex ID: W3152835471 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5016212

StkTokens<i>: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities</i> (Q5016212): Difference between revisions

Latest revision as of 09:34, 30 July 2024

Statements

Identifiers

Sitelinks

Mathematics(1 entry)