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.
|