Frame rules from answer types for code pointers

DOI10.1145/1111037.1111065zbMATH Open1369.68159OpenAlexW2164078934MaRDI QIDQ5348932FDOQ5348932

Authors: Hayo Thielecke 

Publication date: 21 August 2017

Published in: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1111037.1111065

Recommendations

• Types, Maps and Separation Logic
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• A semantic model of types and machine instructions for proof-carrying code
• Types, bytes, and separation logic
• High-level separation logic for low-level code

zbMATH Keywords

polymorphismHoare logiccontinuationstyped assembly languagecode pointers

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cited In (1)

• Reasoning about B+ trees with operational semantics and separation logic

This page was built for publication: Frame rules from answer types for code pointers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5348932)