Typed Operational Reasoning

This semester I’m attending Derek’s course on Typed Operational Reasoning. Description from the site:

While many theorems about type systems are provable by straightforward induction, some properties are much trickier to prove and require a clever insight into how to “strengthen the induction hypothesis”. The method of logical relations provides such an insight, and it has been applied, generalized, and extended to prove a variety of interesting properties about typed programs. These include termination, strong normalization, decidability of type checking, consistency of type equivalence, contextual equivalence of programs, effectiveness of data abstraction mechanisms, and validity of program transformations. We will introduce the idea as it originated–Tait’s method for proving termination/strong normalization for the simply-typed lambda calculus–and eventually work our way up to equational reasoning about programs in a language supporting polymorphism, existential types, recursive functions, recursive types, and mutable references. Although the logical relations method is often used in the setting of denotational semantics, we will focus on how to use it to do operational reasoning about typed programs.

A secondary goal of the course is to convey a sense of how one actually does research and makes progress in programming language theory, or at least how I do it. Although classic results are often presented in the literature without any hint of their origins, in reality there is a continual, subtle interplay between the act of proving theorems and the act of discovering what theorems one wants to prove. (This is closely related to what Lakatos calls “the method of proofs and refutations”.) I will try to convey this interplay in the presentation of a number of topics in the course.

A Step-indexed Semantics of Imperative Objects

Here is the final version of the paper I wrote with Jan as a follow up of my Master’s thesis. I’ll present it at the Workshop on Foundations of Object-Oriented Languages (FOOL’08) on the 13th January in San Francisco. This means I will also attend POPL, with which the workshop is affiliated, and I’m quite excited about it. Anyway, here is the paper and the 64-page extended version with full proofs.

Since the workshop does not count as prior publication the next step for us is to submit a slightly improved version to the Logical Methods in Computer Science journal.

The Connection Between Separation Logic and Program Analysis

Shape Analysis

• Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. Symbolic Execution with Separation Logic. APLAS 2005.
• Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. A Local Shape Analysis based on Separation Logic. TACAS 2006.
• Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. CAV 2007.

Information Flow

• Torben Amtoft, Sruthi Bandhakavi, and Anindya Banerjee. A Logic for Information Flow in Object-Oriented Programs. POPL 2006.

Reading one paper each day, makes the doctor go away

Acknowledgements

Looks that I forgot the most important thing in my last post: thanking the ones who helped me a lot. I entirely mean what I wrote below.

I am profoundly indebted to my adviser, Jan Schwinghammer, for his continuous support during the last year. I thank Jan for his unlimited patience when explaining the basic concepts I needed to know before I could get started with my thesis. Not only did he share with me some of his knowledge and ideas, but also some of his enthusiasm. Our discussions provided much motivation, and radically changed the way I perceive theoretical computer science.

I am grateful to Gert Smolka for his valuable advice given on many occasions, for his inspiring introductions to logic and semantics, and for offering me the opportunity to work with Jan. I also thank Gert Smolka and Holger Hermanns for reviewing my thesis.

Finally, I would like to thank the members of the Programming Systems Lab and the International Max Planck Research School for Computer Science for their friendship and support.

A Line in the Sand

Today I submitted my Master’s thesis, two weeks after the original deadline. The deadline extension really helped me get it into a good shape. On the other hand, in the end the thesis covered only the functional object calculus, even though my stronger results were for the imperative object calculus. Unfortunately it would have taken too long to write everything up. I started with the functional calculus and realized too late there is not enough time for both so that I can set the priorities right. Anyway, the things I presented are self-contained and even without the imperative calculus, the thesis is pretty consistent (69 pages). And hopefully we will manage to publish the stronger results somewhere.

Thesis
Step-indexed Semantic Model of Types for the Functional Object Calculus (623.8KB PDF)

Midlands Graduate School

University of Nottingham, UK, 16 – 20 April, 2007

Towards a Local and Modular Program Logic for Objects

Motivation
There are many application domains where software failures are not an option. Formal methods allow certain properties of systems to be guaranteed: safety, security and even correctness. Depending on the property of interest, verifying a system can be fully automatic, e.g. when using type systems or model checking; or it can be a tedious manual process, as in the case of deductive verification. Still deductive verification plays an important role in the development of dependable software systems, since it can guarantee program correctness, it is not restricted to finite-state systems and can handle unrestricted programs with rich data structures.

IMPRS Master Seminar Talk

Had my talk in the IMPRS Master Seminar yesterday, with the topic: Semantics of Imperative Objects (abstract, slides, notes). And while everybody told me the talk was great, I didn’t feed very comfortable giving it. Since I got lots of feedback from my colleagues, here are some things I should improve:

• Less is more: put less information so that people don’t feel overwhelmed. While I tried my very best to explain everything, it was just too much for most of the people there.
• A little less information would also have allowed me to fit in the allocated 30 minutes – went over them by only around 2 minutes. However, many hungry IMPRS students complained about this.
• Also some of my slides were a little too crowded, this can surely be improved. Also the example I skipped could just not be there, or I should have waited at least for a couple of seconds before moving on.
• Be more relaxed, more natural, less stressed. In this talk (and others as well) I was quite nervous and it showed off: didn’t breath well enough and my speech was not always so fluent, moved my hands too much, I moved back and front a little (well, considering that I’m hyperactive in general this is not that bad), repeated “so”, “OK and “well” maybe too often, and I even bit my finger/nails (really don’t remember doing this). What’s really interesting is that my nervosity showed off more in the beginning of my talk than in the end, while for me the it felt much more stressing at the end, after I had the small battery problem since I was also rushing a little (the timer was reset so I had no clue how much time I have left). I was also less confident about that part since it’s a lot harder but apparently this didn’t show off.
• What people did notice was that I sped up a little in the end, don’t think it was too bad though. But, once again, less information would have helped me maintain a the perfect cruising speed throughout all of my talk.
• The intro, my first two sentences were way too fast, showing that I was really nervous, even though it was hard for me to notice this.
• My eye contact is still not perfect. I didn’t look all over the room, sometimes I found myself pointing at text phrases without any reason, and finally I was looking at Jan for approval when giving one or two of the answers to questions instead of looking at the person who asked.
• Although nobody complained about this (Jan was probably the only person who could notice anyway), I could have given better answers to some of the questions. For example my answer for the FOL vs HOL specifications question was quite vague, I should have mentioned abstract data structures which are possible only with HOL (using abstract predicates). Instead I had the detour about mechanization, which was not so bad, but surely not supporting my claim that HOL specifications are more expressive. I was just not able to find any argument so fast. Maybe I should think a little more before answering. One other question I could have answered better was Marjan’s question about subtyping and polymorphism in a step-indexed semantics. While my answer for the subtyping part was very good, there was also an answer for the polymorphism part that was as simple: in this setting universal types are just intersections over types, while existential types are just unions. However, I read these papers about step-indexed semantics only once and that was a while ago, so I just couldn’t remember this in just 3 seconds. I should definitely focus more on my research, and less on doing abstracts, slides, tutoring, lectures, etc.

An open research question: Is it OK to have detours and should I have wrap-ups in a 30 minutes talk?

Choosing a Proof Assistant

The history of onsound proof rules for Hoare-like logics led me to the desire to do the proofs for my master thesis with the help of a proof assistant (wrongly also named theorem prover). Probably time won’t allow me to do this, but anyway, I already decided that if I need to do interactive proving I will most likely do it in Isabelle/HOL. There are two more systems that are probably worth considering: Coq and Twelf.

Thesis Planning

Month	Thesis	Other
August	read general	Google SOC
September	read particular topics	10 days in Romania, AD?
October	fix topic, official start
November	initial presentation	master seminar (8th)
December	hard work
January	hard work, start writing
February	write thesis
March	submit and present thesis

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.

Learning

I’m in vacation for several weeks now, but that does not mean I’m taking a break from learning. Here is what I currently learn or plan to learn in the very near future:

• More Semantics
  
• Haskell
• Category Theory
• Program Analysis
• Model Checking