ICALP/LICS 2015: Day 3

The third day at ICALP/LICS 2015 was kicked off by a joint ICALP/LICS keynote address delivered by Peter O'Hearn (Facebook and University College London, UK). Peter's talk was entitled From Categorical Logic to Facebook Engineering and described at a high level of abstraction how his work on logic, categories and types led to the development of separation logic and of the algorithmic techniques that his colleagues and he embodied in tools that are now being deployed daily on the Facebook code base.

Peter presented a prime example of tools and techniques from the TCS community that have become mature enough to make a difference for the development of fast-changing code bases like the one at Facebook. Peter took us on a journey that covered a number of concepts from the computer science logician's toolkit, such as categorical logic and model theory, denotational semantics, the Curry-Howard isomorphism, Substructural Logic, Hoare Logic and Separation Logic, abstract interpretation, compositional program analysis, the frame problem, and abductive inference.

His talk was followed by the largest number of questions I have seen asked so far at this conference.

In the afternoon, I attended an ICALP and LICS joint tutorial delivered by Andrew Pitts (University of Cambridge, UK). Andy's tutorial dealt with a very interesting and hot topic, namely Names and Symmetry in Computer Science, a topic to which Andy has devoted a lot of research over the last few years, some of which is covered in this book. I invite you to consult these slides for an idea of what Andy's tutorial covered.

The day ended with a very eventful and inspirational joint award ceremony with talks by Xi Chen (Presburger Award recipient), Igor Walukiewicz (LICS Test-of-Time award recipient) and Christos Papadimitriou (EATCS Award recipient). I will try to write something about that session at some point tomorrow.