Smiling: June 2006

Got a Haircut

Before:

After:

Day of the Open Doors at Dagstuhl

Today we attended the day of the open doors at Dagstuhl. We traveled to Wadern with the bus and it was an enjoyable ride, especially because of the excellent company.

We saw the ruins of the old castle and then got lost in the woods. After a short time we found Dagstuhl and we had traditional food for lunch - the dessert was absolutely delicious. Then we wondered through the castle for some hours. We saw the gardens, some football playing robots from this year's RoboCup (including "Microsoft Hellhound"), the library, a modern art gallery, a chapel and more.

I enjoyed the trip and I'm looking forward to attend CS-related workshops at Dagstuhl one day.

[Edited: Added two more pictures]

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

Separation Logic

Now it's official that the topic of my master thesis will be related to Separation Logic. My supervisor is Jan Schwinghammer from the Programming Systems Lab of the Saarland University.

Last night I couldn't fall asleep until I wrote an email to Jan to tell him about my decision. Telling him was very important because I don't want to be tempted to try escape when I will see how hard these things really are. Now I hardly understand anything about them, but the topic looks promising and very challenging at the same time, and this is more than enough to motivate me to try my best.

Separation Logic is a sub-structural logic that supports local reasoning for imperative programs. It is designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers.

Alice in Wonderland

Alice is a functional programming language based on Standard ML, extended with rich support for concurrent, distributed, and constraint programming. Its developed by the great people of the Saarland University Programming Systems Lab, and it works on a lot of different platforms. However, it does not work on Intel Macs yet, so I tried to package it with Fink. It took a whole night until now and it is still not working.

Enrique Got out of the Hospital

After having talked with a guy from intraNET Systemhaus, I went and picked up my repaired MacBook. They told me that a wire that connected the battery was broken and they have to replace it. Now everything works just fine. Happy, Happy, Joy, Joy!

The Girl From My Dream

The girl from my dream
Tender and sweet
Flying over me
Like a white angel
If only she knew
How dear she is to me

The Little Guy Is in the Hospital

After calling Apple Care, today I received the new battery for the MacBook. Unfortunately this didn't solve anything, so I just called Apple Care again. They told me to bring the little one to their closest support center. That is 4 kilometers from where I live so I had a long ride there. Hopefully they will fix it in three to five working days, and life will return to normal.

The Little Guy Is Sick

The Battery of my two days old MacBook just died this morning. I was using it without the power cord, when it turned off for no apparent reason. Tried to restart it but it didn't work, until I connected it to the power cord. Now it works with the power cord but the battery is not charging, and if I remove the power cord it just turns off. Tried to play with the battery a little but without any success.

Next week is a very full one for me so this was the last thing I needed. However I will try to contanct an Apple service representative to see what needs to be done.