Sunday July 6, 2008 was my first day at ICALP 2008. The conference was commenced the day before with the first day of the Dynamo workshop, but I had to be at a friend's Ph.D. defense session and an affiliated workshop. Thus, I lost the opportunity of being here right from the beginning. But there is Persian proverb which says: no matter when you catch a fish, it is fresh!
My first day was mostly spent at the SOS'08 workshop. It is nice to see fresh blood in the SOS community; there were a couple of graduate and Ph.D. students present at SOS'08 who have just started with SOS as their research subject. A warm welcome to all of them.
What follows is a biased overview of the talks presented in this very interesting workshop. Bartek and Matthew did an excellent job in organizing and chairing SOS'08; thank you very much Bartek and Matthew.
Vincent Danos: solid state concurrency
Vincent presented a general picture of biological systems and their huge dimensions which make any explicit state-exploration technique totally obsolete. He introduced the basics of the Kappa language which provides an abstract model for the (local) rules of interaction among biological agents. He presented a symbolic probabilistic abstraction for such systems (presented at VMCAI'08). There is a strong similarity between the situation here and that of random graphs as studied in statistical physics.
Observation: I found this talk extremely fascinating and very close and related to the ongoing work on the verification of distributed algorithms such as epidemic and gossiping protocols.
Michele Lorieti: Stochastic extension of process calculus, called CASPIS, for service oriented computing (SOC), which are by the way all the rage. The extension adds rates (for a negative exponential distribution) to synchronization constructs, and the rates are calculate in the same way as in PEPA.
Observation: Mixing synchronization with rates makes the semantics very difficult. Perhaps IMC and Markov Decision Processes are the way to go.
Muck van Weerdenburg: Automating soundness proofs
Muck translates SOS rules and the transfer condition for bisimulation into first order logic formulae and then by feeding a witnessing bisimulation relation for each axiom, the proof tool (initially Coq, then replaced by Muck's own proof tool). He has applied his tool . He even has a web-
Observation: Nice work. We need more of this kind of formalized proof environments for SOS.
Gustavo Ospina: Formalisation of C Language Interfaces
I must say I was a bit distracted during this talk. It reported on operational semantics of interfacing between C and another language called Russel, but the details have escaped my mind.
Michel Reniers, SOS with First Order Logic
Michel reported on a nice improvement over our
Bartek and Luca raised the question whether we need such an expressive logic to specify the premises of the SOS rules and whether we can specify the same phenomenon with fragments of first order logic.
Eike Best: Relational Semantics
He presented the relational approach to operational semantics for non-deterministic sequential programs. Then, he presented the standard (denotational) semantics for such programs for both partial and total order semantics using Hoare and Smyth power domains. Then, he gave a generic way of presenting these semantics in a set-theoretic fashion by tailoring the definition of subset relation and relational compositions in each case.
Observation: Very neat talk to the foundations of semantics; reminding me of my first expositions to formal methods.
Dale Miller: Formalizing SOS in Logic
Dale started off by pointing out a dichotomy in the interpretation of computation, namely, computation as model (e.g., function, relation, or LTS) versus computation as deduction (e.g., in lambda calculus and logic programming). Being a logician, he stated his clear preference for the latter interpretation. Then, he gave an overview of syntax, from abstract to concrete, from strings to lambda-trees. Then he gave an introduction to the specification of operational semantics as a logical specification, showing that the traditional treatment of semantics as a logical formulae for nominal formalisms, such as pi calculus, is insufficient for proving impossibility of transitions and as a result bisimulation. He introduced then the nabla operator, as a substitute for universal quantification, which would enable us to prove impossibility of transitions (since it essentially enables us to prove that \lambda x . x cannot be unified with \lambda x .w).
Addendum by Luca: Dale had some great one-liners in his talk. The one I liked best was one he used in his reply to a question from Matthew Hennessy: "The world is too small for two self-dual quantifiers."
Peter Mosses: Implicit Propagation in SOS
SOS specifications often contain "redundant" information, i.e., they carry over lots of information that do not change along a transition or change in a very standand way (the change is propagated from the source of the conclusion to the source of the premise(s) and then from the target of the premises to the target of the conclusion). Peter presented an elegant way of "factoring out" such information and making SOS specs much more readable and also more reusable.
Together with Michel, we presented some initial ideas on writing a textbook about SOS. Peter Mosses suggested creating a wikipedia page for SOS, which is missing at the moment.
P.S.: Arnar updates his photos from ICALP'08 on a daily basis. Thanks to Arnar, Anna, Luca, Magnus and all the organizers for their excellent hard work.
2 comments:
any news what are the best papers in different tracks?
The best paper awards will be announced this evening at the EATCS general assembly. I will post the list after the meeting.
Post a Comment