Frame rules from answer types for code pointers

DOI10.1145/1111037.1111065MaRDI QIDQ5348932zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

code pointerscontinuationsHoare logicpolymorphismtyped assembly language

Mathematics Subject Classification ID

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

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

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)