Loading...
Please wait, while we are loading the content...
Similar Documents
Frame rules from answer types for code pointers.
| Content Provider | CiteSeerX |
|---|---|
| Abstract | We define a type system, which may also be considered as a simple Hoare logic, for a fragment of an assembly language that deals with code pointers and jumps. The typing is aimed at local reasoning in the sense that only the type of a code pointer is needed, and there is no need to know the whole code itself. The main features of the type system are separation logic connectives for describing the heap, and polymorphic answer types of continuations for keeping track of jumps. Specifically, we address an interaction between separation and answer types: frame rules for local reasoning in the presence of jumps are recovered by instantiating the answer type. However, the instantiation of answer types is not sound for all types. To guarantee soundness, we restrict instantiation to closed types, where the notion of closedness arises from biorthogonality (in a sense inspired by Krivine and Pitts). A machine state is orthogonal to a disjoint heap if their combination does not lead to a fault. Closed types are sets of machine states that are orthogonal to a set of heaps. We use closed types as well-behaved answer types. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Answer Type Code Pointer Frame Rule Closed Type Machine State Local Reasoning Type System Polymorphic Answer Type Closedness Arises Simple Hoare Logic Whole Code Assembly Language Main Feature Disjoint Heap Separation Logic Connective Well-behaved Answer Type |
| Content Type | Text |
