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

DOI10.1017/S0956796821000022OpenAlexW3151508267MaRDI QIDQ5016209

Frank Piessens, Dominique Devriese, Thomas van Strydonck

Publication date: 13 December 2021

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796821000022

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (2)

Linear capabilities for fully abstract compilation of separation-logic-verified code ⋮ StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

Cites Work

• Unnamed Item
• Unnamed Item
• Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
• Sound Modular Verification of C Code Executing in an Unverified Context
• Fully-abstract compilation by approximate back-translation
• Abstracting gradual typing
• Fully abstract compilation to JavaScript
• Fully abstract compilation via universal embedding
• Higher-order ghost state
• The Essence of Higher-Order Concurrent Separation Logic
• Featherweight VeriFast
• Gradual Program Verification
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities
• Formal certification of a compiler back-end or
• A verified information-flow architecture
• Shape Analysis for Composite Data Structures
• Runtime Checking for Separation Logic
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Linear capabilities for fully abstract compilation of separation-logic-verified code