Talk Review: A Pictorial Introduction to Separation Logic

Dr. Tony Hoare is a clear and precise speaker. Attending his talk is a great experience.

In this talk, the speaker talks about a new logic that unifies the concepts of pointers, concurrency, weak memory and communication. The speaker starts by defining four degrees of separation between two program traces: 1) they are disjoint traces 2) one is sequentially after another 3) both of the traces can be executed in parallel 4) both the traces are mutually exclusive - they cannot happen together.

It is then seen that 4) => 3) => 2) => 1) - that is, the relation 3) holds whenever 4) holds, 2) holds whenever 3) holds and so on.

"Hoare triples" are then introduced. These are related to the concept that post-condition are true when precondition and invariant of a program are true. The triples can be composed in interesting manners.

Though I did not understand much of what follows because of these results, through google search it seems that these results are useful in proving program correctness. The next day Dr. Hoare presented a topic related to program correctness in another conference.

Presentation slides are here (only about half could be covered in his talk). Further reading keywords: Galois Connections (pdf, pdf), Category Theory, Event Algebra.