This year the (11th) annual IEEE symposium on Logic in Computer Science (LICS) was part of a 4-meeting mela under the banner Federated Logic Conference. The other three were:
There were also several pre- and post-conference workshops: Foundations of object-oriented languages, Partial order methods in verification (POMIV), Teaching logic and reasoning in an illogical world, Computational complexity and programming languages, SPIN (a verification tool), Internet ... . There were three participants from India -- Anil Seth and I, both from IMSc, Madras, and Krishna Rao from TIFR, Bombay (currently visiting MPI, Saarbrucken). I attended POMIV, LICS and a few talks in RTA.
The Kleene award for best student papers went to Juha Nurmonen (Counting modulo quantifiers on finite linearly ordered trees) and Guy McCusker (Games and full abstraction for FPC).
Robin Milner's plenary lecture (a formal occasion, in a grand ballroom of Hyatt Hotel) started off with the differences in emphasis between studying computation and interaction (prescription vs description, and so on). He argued the need for a calculus for interactions with generic rather than ad-hoc notions, and then presented his (and his students') recent efforts towards such a calculus. Milner's generic notions: binding structure, naming and ``boxing''.
Henzinger gave an excellent tutorial on hybrid automata. States usually represent values of system variables, and in hybrid systems, some variables vary continuously. Such systems are presented using conditions on derivatives (a clock is a variable whose derivative is always 1, a stopwatch is a variable whose derivative is always 1 or 0, and so on). Mahler, Manna and Pnueli initiated the study of hybrid systems, and the area has seen good results recently, many by Alur and Henzinger among others. In this tutorial, Henzinger surveyed results on the complexity of reachability and gave intuitive reasons for both positive and negative results, showing how far one can push techniques from discrete-state system theory to mixed systems, and where one needs new ideas.
Joyal's tutorial was on a game-theoretic interpretation of bi-complete categories. The games have three players: two opponents and a mediator. Joyal talked about when the mediator has complete communication strategies (iff the pair of terms on which the game is played are ordered in the free lattice). Equivalent strategies define the same arrow. The amazing (and entertaining part) was that he had examples from share markets. (Indeed, according to gossip from Prakash Panangaden, Joyal is an expert on finance.)
Of what I understood of the finite model theory papers, the one by Kolaitis and Vardi on logics with a fixed finite number of variables was very interesting. Gregory McColm's presentation on zero-one laws for Gilbert-random graphs was more fascinating for the applications of these graphs in biological models and percolation theory than for the main theorem itself. In model checking, the emphasis continued to be on practical verification problems on one hand (QBDDs, reactive modules etc.) and on deepening our understanding of Rabin tree automata on the other. In temporal logic the paper by Etessami and Wilke showing strictness of the until-hierarchy was notable. A number of papers were on decision problems (unification, paramodulation, semi-thue systems, abduction, subtyping dependent types, ... ). Palliath Narendran (Albany) gave a nice talk on polynomials in semirings.
In semantics, the story of full abstraction via game semantics continued on. I should also mention the series of papers by Abbas Edalat and others from Imperial College bringing analytical methods like integration and differentiation into the context of domain theory. This LICS also had a couple of papers of this kind. (During the discussion, Dana Scott remarked: ``I am glad that at last, after 20 years, someone is doing the kind of mathematics domain theory was meant for''.)
Type theory had, as usual, papers on subtyping and polymorphism. (I was surprised to see very few papers on linear logic in this year's LICS; one of these few was very amusingly presented by Phil Wadler (Glasgow)). Ong (Oxford and Singapore) had an interesting paper which addressed the question of which category corresponds to classical proofs (in the same way as cartesian closed categories capture intuitionistic ones).
In the concurrency session, Ian Stark (Aarhus) gave a very nice presentation on a domain model for the $\pi$-calculus. Among the other presentations, one high point was an exchange between Vladimiro Sassone (Pisa) and Rob van Glabbeek (Stanford) on what constituted a degeneracy.
The next LICS (to be chaired by Glynn Winskel) will pair with CONCUR in Warsaw.
This workshop, organized by Gerard Holtzmann, Doron Peled and Vaughan Pratt, was an attempt to bring together researchers from both the concurrency and verification communities with the specific idea of discussing partial order theory in the two contexts. The workshop was held at Princeton from July 24 to 26.
There were only about 50 participants, almost everyone an active researcher in a related area, with nearly half being speakers (there were 24 invited presentations). This meant that more often than not, the audience was actually following what the speaker said! There was a great deal of discussion and interaction, and in this respect, this was one of the best workshops I have ever attended. (Rob van Glabbeek could always be relied on for interesting questions; one talk saw a remark (not by Rob): ``Can you please show that slide again $\ldots$ do the last three lines mean anything at all?'')
In my opinion, the workshop demonstrated the state of the art rather clearly. We understand partial-order based models of concurrency reasonably well (Glynn Winskel and Mogens Nielsen gave nice unifying presentations on these, with van Glabbeek and Pratt making a case for studying observations of partial orders). Identifying regular behaviours is hard (a convincing demonstration in the context of branching behaviours by Thiagarajan, and an excellent exposition on automata which accept partial orders---rather than strings or trees---by Wolfgang Thomas). On the logic side, there is darkness---what is a good logic, amenable to such methods? how much expressiveness can we get? ... (a clear elucidation by Rajeev Alur, and a wide-ranging survey by Allan Emerson). Current proof methods are inadequate (the presentations by Katz and Reisig were more interesting for the problems they pointed out than their own solutions). On the practical front, there is a feeling of frustration (a typical reaction is, ``OK, we can do this, but how far can we push these techniques?'').
Doron Peled hopes that this workshop is the beginning of a series and that others will take it up. I don't know about that, but there are many interesting unanswered questions here and these will certainly keep researchers occupied for a while yet.