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

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: