Possible Directions

Here are some directions I could follow in my thesis. First two were suggested by Jan, while the last came to me while attending the Trustworthy Software Workshop some weeks ago.

The first idea is about Separation Logic for a call-by-value functional language like Standard ML. A similar logic has been developed in a recent paper by Birkedal and others, but for the language Idealized Algol which is call-by-name and has a distinction between imperative computation (at base type command only) and higher-order one.

The second idea is about extending a logic for the object calculus (of Abadi and Cardelli) by Separation logic. Jan considered this logic (originally due to Abadi and Leino) in his PhD where he proved soundness, but so far there is no local reasoning in that there is no separation connective and no frame rule. The obvious question is - can it be done? There has also been some work on mechanizing this logic in a theorem prover (Hofmann and Tang), so once the logic is settled one could try to implement this extension, too. And then there's the question of soundness of any such extension which is likely to be a difficult work.

Last idea is about extending this logic to a (subset of) C0, which is the subset of C used in the Versoft project.

More info:
- Jan's Article
- Murat Baktiev's Thesis