Desperately Seeking Mathematical Truth

The August issue of the Notices of the AMS includes an opinion piece entitled "Desperately Seeking Mathematical Truth" by Melvyn B. Nathanson. At the risk of oversimplifying the message in that opinion piece, the gist of the article can be summarized as follows, using direct quotes from Nathanson's opinion piece.

• "Our knowledge of the truth of a theorem depends on the correctness of its proof and on the correctness of all of the theorems used in its proof. It is a shaky foundation" because "many great and important theorems don’t actually have proofs. They have sketches of proofs, outlines of arguments, hints and intuitions that were obvious to the author (at least, at the time of writing) and that, hopefully, are understood and believed by some part of the mathematical community."
• Recognizing mathematical truth is harder than one might think at first. "If a theorem
  has a short complete proof, we can check it. But if the proof is deep, difficult, and already fills 100 journal pages, if no one has the time and energy to fill in the details, if a “complete” proof would be 100,000 pages long, then we rely on the judgments of the bosses in the field. In mathematics, a theorem is true, or it’s not a theorem. But even in mathematics, truth can be political."

So, mathematical truth is the result of a social process. (I'd rather not say "political".) A theorem is proven when a sufficient portion of the mathematical community agrees that its proof is convincing and starts building on it, despite the absence of a "complete" proof. I do not find this a particularly controversial or novel opinion, and I am sure that it has been aired before. What I find utterly remarkable is the apparent robustness of the notion of mathematical truth that arises from the aforementioned social process.

Yes, proofs of several published theorems contain mistakes. However, more often than not, the mistakes can be fixed and the results turn out to live to see the day after all.

Of course, I expect that mathematicians will want to improve upon the social notion of proof that underlies their profession. Quoting again from the opinion piece by Nathanson:

We mathematicians like to talk about the “reliability” of our literature, but it is, in fact, unreliable.

Part of the problem is refereeing. Many (I think most) papers in most refereed journals are not refereed. There is a presumptive referee who looks at the paper, reads the introduction and the statements of the results, glances at the proofs, and, if everything seems okay, recommends publication. Some referees do check proofs line-by-line, but many do not. When I read a journal article, I often find mistakes. Whether I can fix them is irrelevant. The literature is unreliable.

How can the reliability of mathematical proofs be improved? When should a proof be deemed to be "complete"? As a computer scientist, I'd say that a proof is really "complete" when it can be verified by a computer-based proof checker and it has been independently verified using a few such software tools. I know that this is a very stringent requirement, which will most likely never be implemented, but either we are ready to accept that mathematical truth is an unreliable but remarkably robust notion or we enlist the help of our computers to try and make it more reliable.

Do any of you think that proof-checking of research-level mathematical proofs will become commonplace in our lifetime?

Addendum dated 5 August 2008: I should have known that Doron Zeilberger would have commented on Nathanson's opinion piece. Of course, Dr. Z's opinion is thought provoking as usual. You can read it here. In summary, Dr. Z suggests two ways for improving the reliability of mathematical knowledge.

1. In his words, "First computerize! Computers are much more reliable than humans, and as more and more mathematics is becoming amenable to computer checking, this is the way to go."
2. Abandon anonymous refereeing.

I have already expressed support for the first suggestion in my original post, as have some commentators in their very thoughtful comments. (I really appreciated them, and I hope to reply to them soon.)

Regarding the second suggestion, I am not so sure that abandoning anonymity in refereeing would have such a great effect on the reliability of mathematical literature. The bottom line is that one should exercise the greatest amount of professionalism in all aspects of the academic profession, regardless of whether one does something anonymously or not. Excellent referees are a great resource to have, and editors and PC members soon build a trusted core of referees that can be relied upon to provide high-quality feedback to authors and editors alike. Referees who do not do a good job tend to be ignored after a while, as do editors who act as black holes for the papers that are submitted to them.

Third ICE-TCS Annual Report

The third ICE-TCS annual report has been available since June 12, but I never mentioned its availability on this blog. If you are interested in keeping abreast of what is happening in our little TCS centre here in Reykjavík, do have a look.

Some of the people who attended ICALP 2008 asked us what we are going to do with the centre when funding runs out. Our answer was, "What funding?" The centre operates with very few resources and without specific funding to support its activities. We try to raise money in ad hoc and haphazard ways.

The Icelandic Fund for Research announced the availability of centre-building funding for the first time ever last spring. A consortium led by ICE-TCS sent in a pre-proposal, but our expression of interest was not one of the ten that were selected for further consideration, alas. Such is life, I guess, but, if I may say so, the list of ten selected pre-proposals is somewhat surprising on purely scientific grounds and hardly fulfils the requirements concerning international collaboration. (Our pre-proposal had BRICS, CISS, FUNDIM and the Centre for Computational Molecular Biology at Brown University as some of its cooperating centres.)

Anyway, we will try to maintain a decent level of activity in TCS on this remote, but rather attractive, island in the north Atlantic :-) For present activity on another much smaller, but also much hotter, island, see Luca Trevisan's in theory.

General Assembly of the EATCS at ICALP 2008

The EATCS holds its annual General Assembly (GA) during ICALP. This year's GA was held during ICALP 2008 on Tuesday, 8 July, after Peter Winkler's master class on mathematical puzzles. I have already covered some of the highlights of the GA in earlier posts (e.g., the best paper awards for ICALP 2008 and the proposed new young research prize in TCS). Here I will limit myself to highlighting a few of the many issues under discussion within the EATCS Council that you might be interested in commenting on. In general, the EATCS strongly encourages feedback and suggestions from the members of the TCS community at large. I will pass on to the Council any suggestion/comment/criticism you might have.

First of all, here are some statistics presented by Leslie Ann Goldberg regarding track A of ICALP 2008. Track A had 133 submissions that could be classified as dealing with Design and Analysis of Algorithms, 87 for Complexity Theory and 67 under the heading Approximation. The most successful topic as far as percentage of acceptances was concerned was Quantum Computation (6 selected out of 14 submissions, 43% selection rate); Randomness was second with 15 selected out of 39 submissions (38% selection rate). Overall, Germany, Israel and the USA contributed 120 submissions to track A.

For track B, there were 8 selected papers under the heading Verification, 7 on Words and Trees and 6 on Logic and Complexity. Germany and France led the number of authors with 39 and 39 authors each. The UK, the USA and Italy were next in line with 32, 29 and 25 authors, respectively. Spain was next with 13 authors.

No comparable statistics were presented for track C. However, Ivan Damgaard remarked that it was noteworthy that no accepted paper for track C dealt with the formal specification and verification of security protocols.

The General Assembly approved the suggestion of the Council that ICALP 2010 be organized in Bordeaux, France. Igor Walukiewicz presented the bid from Bordeaux, highlighting many reasons for having ICALP there. The GA also discussed possible alternatives for ICALP 2011. In particular, Giorgio Ausiello mentioned that the sister society AAAC (Asian Association for Algorithms and Computation) has invited ICALP to Japan. Concerning 2012, Giorgio Ausiello mentioned that, in the occasion of the centennial of Turing's birth, a special event should take place in Cambridge, UK. The EATCS is considering the co-location of ICALP 2012 with the events in the Turing centennial.

Jan van Leeuwen reported on possible connections netween the EATCS and Computability in Europe, a new association that "aims to widen understanding and appreciation of the importance of the concepts and techniques of computability theory, and to support the development of a vibrant multi-disciplinary community of researchers focused on computability-related topics."

The EATCS Council has formed a new publication committee which I have been asked to chair. Apart from me, the committee will consist of Josep Diaz, Juhani Karhumaki, Burkhard Monien, Catuscia Palamidessi, Valdimiro Sassone and Maria Serna (the new editor of the Bulletin of the EATCS). One of the important roles that this committee will have is to propose future developments for the Bulletin, which is the flagship publication of the EATCS. I would be very happy to hear your opinions on and wishes for the BEATCS.

Amongst the many developments within the EATCS let me finish by mentioning that the EATCS Council has decided that the Secretarial Office will move to CTI. The Secretarial support will be partly paid by EATCS, partly sponsored by CTI. The experiment will be carried on for a period of three years. An important role that the new Secretarial Office will play is in maintaining an ongoing connection between the EATCS and its members. The latest membership figures show a worrying decrease in the number of members at a time when the EATCS needs the support of the TCS community to foster its increasing number of high-profile activities. The number of members of the EATCS has gone down from 1036 in 2006 to 882 in 2007, and has hit an all-time low in 2008 (with 678 members). I hope that the success of ICALP 2008 will help the association a little.

Many photos from ICALP 2008 are available by following the links from this web page.

CadiaPlayer Strikes Again

About one year ago, CADIAPlayer, developed by Yngvi Björnsson and his MSc student Hilmar Finsson within CADIA, our centre for AI research won the General Game Playing (GPP) competition at AAAI 2007. (The aim of the GGP competitions is to help develop systems that can accept a formal description of an arbitrary game and, without further human interaction, can play the game effectively.)

I am happy to report that, in a repeat of last year's final, CadiaPlayer confirmed its world-champion status in GGP at AAAI 2008 in Chicago by defeating ClunePlayer from the University of California, Los Angeles. (ClunePlayer has now been runner-up for three years in a row, and was the world champion in 2005.)

This is great news for the School of Computer Science at Reykjavík University. Congrats to Yngvi, Hilmar and Gylfi.

June Issue of the Bulletin of the EATCS

Continuing the open access policy of the EATCS, the June issue of the BEATCS is now available here for free download. I trust that you will find something of interest to you in this volume, which also features a little technical contribution by your truly.

Let me take this opportunity to encourage all of you to become members of the EATCS. Becoming a member is cheap (30 €) and easy. Moreover, by becoming a member you will support the activities of the TCS community at large not just in Europe, but across the world. These are busy times for the EATCS, and the organization needs your support to thrive.

For instance, I can tell you that, during its meeting at ICALP 2008 in Reykjavík, the EATCS Council decided to create a new Award for Young Researchers. The new award committee of the EATCS will soon define the details for the prize. The EATCS aims at having the rules set by ICALP 2009, so that after that conference, it can distribute the call for nominations, appoint the evaluation committee and set the deadlines with the aim to deliver the award for the first time at ICALP 2010. More news on the EATCS General Assembly held at ICALP 2008 will follow soon.

Some Recent Awards

A few awards and prizes have recently been handed out to members of the TCS community.

The LICS test-of-time award 2008 has been given to Martín Abadi and Leslie Lamport for their paper The Existence of Refinement Mappings. In Lamport's own words:

The method of proving that one specification implements another by using a refinement mapping was well-established by the mid-80s. ..... It was known that constructing the refinement mapping might require adding history variables to the implementation. Indeed, Lam and Shankar essentially constructed all their refinement mappings with history variables. Jim Saxe discovered a simple example showing that history variables weren't enough. To handle that example, he devised a more complicated refinement-mapping rule. I realized that I could eliminate that complicated rule, and use ordinary refinement, by introducing a new kind of dummy variable that I called a prophecy variable. A prophecy variable is very much like a history variable, except it predicts the future instead of remembering the past. (Nancy Lynch later rediscovered Saxe's rule and used it to "simplify" refinement proofs by eliminating prophecy variables.) I then remembered a problematic example by Herlihy and Wing in their classic paper Linearizability: A Correctness Condition for Concurrent Objects that could be handled with prophecy variables.

This paper was my first collaboration with Abadi. Here's my recollection of how it was written. I had a hunch that history and prophecy variables were all one needed. Abadi had recently joined SRC, and this seemed like a fine opportunity to interest him in the things I was working on. So I described my hunch to him and suggested that he look into proving it. He came back in a few weeks with the results described in the paper. My hunch was right, except that there were hypotheses needed that I hadn't suspected. Abadi, however, recalls my having had a clearer picture of the final theorem, and that we worked out some of the details together when writing the final proof.

I had just developed the structured proof style described in [100], so I insisted that we write our proofs in this style, which meant rewriting Abadi's original proofs. In the process, we discovered a number of minor errors in the proofs, but no errors in the results.

The first CAV award has just been given to Rajeev Alur and David Dill for the invention of the formalism of timed automata. See the full announcement for more details. This is a well deserved recognition to Rajeev and David for a fundamental contribution to the theory of real-time systems verification. Timed automata have been the subject of extensive theoretical investigation since the original paper by Rajeev and David and form the basis for software tools for the specification and verification of real-time systems such as Uppaal. Readers who are interested in a leisurely introduction to the basic theory of timed automata might wish to read part II of this book.

Finally, the European Mathematical Society (EMS) awarded its prizes at the 5th European Congress of Mathematics, held this week in Amsterdam (The Netherlands). The EMS prizes are awarded to young researchers not older than 35 years, in recognition of distinguished contributions in mathematics, and are presented every four years at the European Congress of Mathematics. One of the recipients of the EMS prizes is Assaf Naor, who is honoured for "his groundbreaking contributions to functional analysis, the theory of algorithms, and combinatorics".

Congrats to the award recipients!

Leslie Valiant's EATCS Award Talk

An anonymous comment to my previous post on ICALP 2008 asked

I'm very curious what Valiant talked about Evolution, Intelligence and Human Brain. In particular if he said anything concrete.

Here are some recollections I have from Leslie Valiant's talk. I apologize if I have misinterpreted the main messages from his presentation.

Leslie started his talk by recalling that the first conference he ever attended was ALP 1972 in Paris, which would later become the first ICALP conference. He also quoted an excerpt from the preface of the proceedings for that conference, which I did copy verbatim, written by Maurice Nivat:

“If I were asked, in this preface, to explain how each of these forty five papers contributes to the solution of the main problems in Computer Science, I would be very embarrassed."

I leave it to you to interpret this quote :-)

The bulk of Leslie's presentation was supposed to deal with three topics that interest him right now, namely:

1. Evolution
2. Intelligence
3. Human Brain.
   

The third topic, however, was not addressed during the talk for lack of time.

Regarding evolution, Leslie Valiant remarked that in the 19th century Darwin and Wallace posited an algorithmic mechanism for evolution: “random variation and natural selection.” Up to this day, there are no serious rivals to the Darwin/Wallace theory, but computer simulations of “random variation and selection” offer rather unimpressive results in evolving complex mechanisms.

Leslie mentioned the "quantitative mystery" behind evolution:

1. How can such wonderful 3 billion length DNA strings be found in only 3 billion years?
2. Does evolving complex circuits take exponential time?

In an effort to provide answers to these questions, Leslie compared evolution with learning, and mentioned that evolution can be treated as a form of computational learning from examples in which the course of learning is influenced only by the fitness of the hypotheses on the examples, and not by the specific examples. He explicitly mentioned work presented in a paper of his (see here) and in the recent paper

V. Feldman. Evolvability from learning algorithms, Proc. 40th ACM Symposium on Theory of Computing (2008).

Regarding intelligence, Leslie started by asking

What are people good at that computers are bad at?

His answer was "common-sense knowledge". He then provided the example of word completion (that he used in some recent experiments) and introduced the concept of robust logic, which he introduced about eight years ago. In his own words:

Robust Logic gives a common semantics for learning and reasoning, polynomial time algorithms for both, and soundness and completeness for reasoning.

Leslie described a recent experiment he carried out with Michael in which they developed a system to analyze about 500,000 sentences from the Wall Street Journal. They used a parser to find the structure of the sentences, learned rules to predict erased words and investigated whether chaining these rules leads to an improvement over baseline methods in predicting missing words. The results were a little better than those obtained using baseline methods.

Leslie concluded by saying that we need good "teaching material" for systems like the one Michael and he developed.

ICALP 2008

ICALP 2008 is now over, but the last six satellite workshops will take place over the coming week-end. MohammadReza Mousavi has already reported on some of the talks at the conference in a series of guest posts. Here I will just limit myself to a few remarks on the main events that took place since Wednesday. I will try to devote future posts to some of the other news from the conference.


On Wednesday, Bruno Courcelle (Labri, Universitè Bordeaux, France) delivered a plenary invited talk entitled Graph Structure and Monadic Second-order Logic: Language Theoretical Aspects. Courcelle is one of the 15 most cited French scientists and the most cited French computer scientist. (See http://www.labri.fr/perso/courcell/PrixCitations2004.doc.) In addition, he has become a member of the very prestigious Institut Universitaire de France (see http://iuf.amue.fr/author/bcourcelle/). Courcelle is one of the grand "old" men in theoretical computer science. In a career spanning about 35 years he has given fundamental contributions to the study of the logical, language-theoretic and algorithmic aspects of the theory of graphs. He is also one of the founders of, and main contributors to, algebraic semantics. In his talk, Bruno described the role that hierarchical decompositions and Monadic Second-order Logic play in the extension of methods and results from classic Formal Language Theory to the description of sets of finite graphs. Bruno is putting the final touches to a monograph on this topic that will be published by Cambridge University Press. (Present state of the work Part 1 : Chapters 1-6. Part 2 : Chapters 7-11.)

The scientific programme on Thursday was kicked off by an invited plenary talk by Peter Winkler (Dartmouth, USA). The talk, entitled Optimality and Greed in Dynamic Allocation, described a method for proving optimality in dynamic allocation problems that relies on the assumption that "it's right to be greedy." The method was developed while Peter was working on two problems which arose at Lucent Technologies.


The scientific programme for Thursday reached its climax with the award ceremony, during which the EATCS award and the Gödel prize where handed out. After receiving the EATCS award, Leslie G. Valiant (Harvard, USA) delivered an excellent 30-minute presentation focusing on three topics that interest him right now. The topics are:

1. Evolution
2. Intelligence
3. Human Brain.
   

In his opinion, all these topics are computer science and are screaming for an understanding based on algorithmic approaches. Leslie described some of his work in this direction.

The Gödel prize talk, delivered by Daniel A. Spielman (Yale, USA), provided an outstanding finale for the day. In his talk, Dan explained the idea of smooth anallysis, how Teng and he thought of it and what he hopes the future will bring. Shang-Hua Teng (Boston University, USA) gave a personal and heartfelt introduction to the work they did to merit such a prestigious award.

The main event during the final day at ICALP was an invited plenary talk delivered by Javier Esparza (Technische Universität München, Germany). Javier's presentation was entitled Newtonian Program Analysis and presented recent work by his students and him that aims at using a computational approach to solving equations developed by Isaac Newton about 300 years ago in the analysis of computer programs. The talk presented exciting work and was beautifully and enthusiastically delivered. After the talk, Peter Winkler commented to us: "You saved the best for the last!" Javier closed the talk by saying that "Newton did it all 300 years ago, but he never saw Iceland!"

Dijkstra Prize 2008 to Baruch Awerbuch and David Peleg

During the meeting of the EATCS Council at ICALP 2008, I learned that the Dijkstra Award Committee has selected Baruch Awerbuch and David Peleg as the recipients of this year Edsger W. Dijkstra Prize in Distributed Computing. The price is given to them for their outstanding paper: "Sparse Partitions" published in FOCS 1990.

The prize is given for outstanding papers on the principles of distributed computing, whose significance and impact on the theory and/or practice of distributed computing has been evident for at least a decade. The Prize includes an award of $2000.

My Third Day @ ICALP 2008 (Guest Post by MohammadReza Mousavi)

This is the third guest post by MohammadReza Mousavi on ICALP 2008.

Ran Canetti: Composable Formal Security Analysis (Invited Speech)

Ran underscored the fact that the most challenging part of verifying security is to guarantee that protocols remain secure when put in arbitrary contexts and composed with other protocols. He defined a notion of security which basically requires that the observational behavior of a protocol in the presence of an "environment" machine (which can interfere in all possible ways) emulates the behavior of a perfectly secure protocol with a trusted third party. Combining symbolic methods with concrete cryptographic protocols is another aspect of composition theorem. Explicit analysis of all possible combination of such protocols is infeasible.

The message of the talk can be nicely summarized in the following nice quote (unfortunately forgot from whom):

"In security, the sum of the parts is a hole."

Addendum from Luca: Ran attributed the above quote to Dave Safford.

Patricia Bouyer: On Expressiveness and Complexity in Real-time Model Checking

Metric Temporal Logic (MTL) is a popular extension of Linear Temporal Logic (LTL) with quantitative timing, for which model-checking problem over dense-time models is undecidable. The main culprit for the undecidability is the presence of punctuality, i.e., formulae in which one can talk about exact time moments of events. Thus, punctuality-free fragments of MTL, such Metric Interval Temporal Logic (MITL), are proposed which are decidable. Patricia introduced a new subset of MTL, called coFlat-MTL, which can express properties such as global invariance, bounded response, and some kinds of punctuality (e.g., punctual response), for which model-checking over timed-automata models is in EXPSPACE. She also gave a tableau construction algorithm for this logic.

Antonin Kucera: Controller Synthesis and Verification of Markov Decision Processes

Antonin first showed why we need randomized and history dependent strategies (even bounded memory is insufficient) to control CMDP in order to satisfy qPCTL formulae. Then he presented a study of the complexity of the controller synthesis problem for Markov Decision Processes, which is the following question:

Is there a history dependent randomized strategy such that a given model satisfies a given qPCTL(*) formula?

(qPCTL is an extension of CTL, which allows for specifying properties like: with a probability less than .5, a state with a certain property will be reached.) According to his study, if I remember well, the controller synthesis problem for qPCTL(*) formulae is (2-)EXPTIME-complete in the size of the formula and polynomial in the size of the MDP.

Best Paper Awards at ICALP 2008

The best paper awards for ICALP 2008 were delivered this evening during the EATCS General Assembly.

The best paper award for track A went to the paper The complexity of Boolean formula minimization by David Buchfuhrer and Christopher Umans. The best student paper for track A was given to Jeff Phillips for his paper Algorithms for epsilon-approximations of Terrains.

The awards for track B were made to the papers

• Mai Gehrke, Serge Grigorieff and Jean-Eric Pin. Duality and equational theory of regular languages (best paper) and
  
• Christian Mathissen. Weighted Logics for Nested Words and Algebraic Formal Power Series (best student paper).

Finally the best paper award to track C went to the paper Making classical honest verifier zero knowledge protocols secure against quantum attacks by Sean Hallgren (Penn State University), Alexandra Kolla (UC Berkeley), Pranab Sen (Tata Institute) and Shengyu Zhang (Caltech). No paper qualified for the best student paper for track C.

There is a lot more to report from the conference, but time is short right now. Let me just point out that today ICALP 2008 featured a very special event, which was attended by about 300 participants, including the Icelandic Math Olympiad team, high school teachers of mathematics and members of the public at large. Peter Winkler (Dartmouth, USA) delivered a truly outstanding master class on mathematical puzzles entitled Puzzles You Think You Must Not Have Heard Correctly. It is the first time that ICALP features this type of event bringing a TCS conference of this calibre to a wider audience. Anna, Magnús and I are very happy to see how well it all went. Thanks to Peter for a truly inspirational talk!

When Peter presented the "Boxes in Boxes" puzzle, he said that

At many train stations, post offices and currier services around the world, the cost of sending a
rectangular box is determined by the sum of its dimensions; that is, length plus width plus height.

Magnús remarked that this is definitely true in Iceland for all train stations here. This is an example of logic at its best, and I'll use it next time I have to teach universal quantification over an empty set :-)

My Second Day @ ICALP 2008 (Guest Post by MohammadReza Mousavi)

This is the second guest post by MohammadReza Mousavi on ICALP 2008. Thanks to Mohammad for contributing this post! Further information on ICALP may be found at /dev/collective. See here for photos from the conference.

Track B of ICALP started today (7 July) afternoon. My body is not yet totally accustomed to the 24-hours-light scheme here in Reykjavik and thus, I decided take a leave from the morning sessions of Tracks A and C. What you read is a summary of a few talks given at Track B this afternoon. Some of the talks went beyond my limited understanding of their subject matters and thus, you may find inaccuracies in my report of the results, for which I apologize in advance.

Wim Martens: NFA Minimization

There exist well-known efficient state-minimization algorithms for DFA's. It is also known that bisimulation reduction for NFA's is efficient but it does not give you the minimal-state NFA. If I got it well, the bottom line, partially established by the ICALP'08 paper, is that all "interesting" state-minimization problems to non-DFA's (e.g., DFA's with multiple starting states or multiple, no matter how few, transitions with the same label) are NP-hard. By interesting Wim means, if I understood well, those minimizations that can lead to exponential reduction in size.


Hermann Gruber: RE Size

The minimal size of the regular expression for an automaton is known to be exponentially larger than the number of states, given that the alphabet is sufficiently large (due to Ehrenfeucht and Zeiger, JCSS, 1976; preprint available from here). In the present paper, the same result is extended to the case where the alphabet contains at least two elements.

Magnus Johansson: Extended Pi

Magnus presented an interesting extension of Pi in which names are replaced by arbitrary terms which can be equated using arbitrary equational theories (satisfying certain natural properties such as equivariance and equivalence) and also, aliasing for arbitrary terms is allowed (aliasing, or active substitution, basically introduces a new equation). The notion of bisimulation that comes with this this calculus (calculi, parameterized by the equational theory), is a very natural one: it requires the aliases of the two processes to be the same (up to the present equational theory) and the two processes to show the same behavior even under equational theories extended with new equations.

My First Day @ ICALP 2008 (Guest Post by MohammadReza Mousavi)

I am happy to provide a guest post by MohammadReza Mousavi, one of the workshop co-organizers for ICALP 2008, on his first day at ICALP 2008. Thanks to Mohammad for contributing this post!

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-interface for his prototype.

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 joint SOS'07 paper on extending SOS with quantifiers. In his paper (joint with Muck van Weerdenburg), he presents a framework and congruence format for SOS which supports first order logic formulae (with infinitary conjunction) in the premise of the deduction rules.

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.

ICALP Coffee Directions

I guess that some of you will be looking for very good coffee places in Reykjavík close to the conference site. If so, you should definitely follow the ICALP coffee directions, courtesy of Pall Melsted. I can vouch for their accuracy, but read also my comment on his post.

By the way, Páll has his own blog, aptly called With High Probability. Link to it!

If I have time, I will try to post some information on eating out in Reykjavík. Any suggestions Páll?

Final ICALP 2008 Update

ICALP 2008 is now really upon us. The scientific feast will begin at 14:00 GMT on Friday, 4 July, with the start of the Second Training School on Algorithmic Aspects of Dynamic Networks (DYNAMO 2008) and will continue until Sunday, 13 July. The ICALP conference proper will be held in the period 7-11 July.

There are a little over 300 people signed up for ICALP and over 150 other colleagues will attend only some of the satellite events. This makes ICALP 2008 one of the best attended editions of the conference ever.

Full details about the conference and its 12 affiliated pre- and post-conference events are available at http://www.ru.is/icalp08. (See http://www.ru.is/icalp08/workshops.html for the workshops.) The programme of talks for the main conference may be found at

• http://www.ru.is/icalp08/icalp2008programme.pdf (detailed programme) and
• http://www.ru.is/icalp08/ataglance.pdf (programme at a glance).
  

The DYNAMO School will feature

• Comprehensive lectures (4h) on
  • Game Theory: Elias Koutsoupias (University of Athens)
  • Online Algorithms: Susanne Albers (Freiburg University)
  • Peer-to-Peer: Christian Scheideler (Technical University of Munich) and Stefan Schmid (ETH Zurich), as well as
    
• Introductory lectures (1h) on
  • Graph Searching: Fedor Fomin (University of Bergen)
  • Self-stabilization: Shlomi Dolev (Ben-Gurion University of the Negev)
  • Internet traffic: Philippe Robert (INRIA Rocquencourt)
  • Network Coding: Christina Fragouli (EPFL).
    

The programme of DYNAMO is available at http://www.liafa.jussieu.fr/~pierref/COST/programme.pdf.

The ICALP conference will have a very rich programme of contributed papers, which were selected from the programme committees from the 472 submissions they received. Here I limit myself to listing the invited talks that will be delivered at the conference and its affiliated workshops.

Sunday, 6 July, 2008:

08:40-09:30 M. Sotomayor, My encounters with David Gale (Match-up, Room 201)
09:00-09:45 Ashish Goel: Incentives based robust reputation and recommendation systems (Foundations of Information Management in Networks, Room 233)
09:00-10:00 Vincent Danos. A stochastic calculus of binding -- applications to the modelling of cellular signalling (SOS, Room 231a)
09:00-10:00 Andrej Bauer. Mathematically structured but not necessarily functional programming (MSFP, Room 235)
09:45-10:30 Maurizio Lenzerini: Integration and filtering of heterogeneous information (Foundations of Information Management in Networks, Room 233)
11:00-11:45 Muthu Muthukrishnan: Streaming and sampling algorithms for information aggregation in networks (Foundations of Information Management in Networks, Room 233)
11:00-11:50 K. Mehlhorn, Assigning papers to reviewers (Match-up, Room 201)
11:45-12:30 Giuseppe Persiano: Security of networks of low capability devices (Foundations of Information Management in Networks, Room 233)
14:00-14:45 Christian Scheideler: Algorithms for scalable and robust information systems (Foundations of Information Management in Networks, Room 233)
14:00-14:50 A. Roth, Kidney exchange: design and evolution of a computer-assisted matching mechanism (Match-up, Room 201)
14:00-15:00 Joseph Sifakis. Component-based construction of heterogenous real-time systems in BIP (Joint ICE and SOS, Room 231a)
14:00-15:00 Dan Piponi. Some elementary algebra and calculus of types and "antidiagonal" types. (MSFP, Room 235)
16:00-17:00 Dale Miller. Formalizing SOS specifications in logic (SOS, Room 231a)

Monday, 7 July, 2008:

09:00-10:00: Muthu Muthukrishnan, Internet Ad Auctions: Insights and Directions (ICALP, Room 131a-b)

Tuesday, 8 July, 2008:

09:00-10:00 Ran Canetti, Composable Formal Security Analysis: Juggling Soundness, Simplicity and Efficiency (ICALP, Room 131a-b)
16:30-18:00 Peter Winkler, Masterclass on Mathematical Puzzles (ICALP, Room 131a-b)

Wednesday, 9 July, 2008:

09:00-10:00 Bruno Courcelle, Graph Structure and Monadic Second-order Logic: Language Theoretical Aspects (ICALP, Room 131a-b)

Thursday, 10 July, 2008:

09:00-10:00 Peter Winkler, Optimality and Greed in Dynamic Allocation (ICALP, Room 131a-b)
16:30-18:00 Award ceremony, including talks by

• Daniel A. Spielman (Yale, USA) and Shang-Hua Teng (Boston University, USA)) --- Recipients of the 2008 Gödel Prize
• Leslie G. Valiant (Harvard, USA) --- Recipient of the 2008 EATCS Award
  

Friday, 11 July, 2008:

09:00-10:00 Javier Esparza, Newtonian Program Analysis (ICALP, Room 131a-b)

Saturday, 12 July, 2008:

09:15-10:15: Roger Wattenhofer. Algorithms for sensor networks, what is it good for? (Algosensors, Room 231a)
09:30-10:30 Terry Rudolph: Quantum computing, matrix permanents and why Bob Coecke isn't the only person who gets to do quantum mechanics by drawing trivial looking graphs (Quantum Physics and Logic/Development of Computational Models, Room 201)

Sunday, 13 July, 2008:

09:00-10:00: Helmut Schwichtenberg. Decorating proofs. (Classical Logic and Computation Invited, Room 233)
14:00-15:00: Stéphane Lengrand. Inhabiting negative types. (Classical Logic and Computation Invited, Room 233)
16:00-17:00 Andreas Winter: The Mother of All Protocols: Restructuring Quantum Information's Family Tree (Quantum Physics and Logic/Development of Computational Models, Room 201)

As you can see, there is going to be an embarrassment of riches and it won't be easy to choose what invited talks to attend during the workshop days.

My co-organizers and I hope that the participants will enjoy all aspects of the conference. In pure scientific fashion, I will keep my fingers crossed until the event is over :-)

If you are participating in ICALP and you'd like to provide guest posts reporting on the conference, send them to me and I'll be happy to post your contributions. It is highly unlikely that I will have time to post anything myself, apart from possibly reports on the EATCS General Assembly and on the Award Ceremony. In fact, as a local organizer, I wonder how many talks I'll be able to attend myself.

Despite the stress of being a local organizer, I am looking forward to this event.