Job Announcement: Dean of the School of Computer Science at Reykjavík University

The School of Computer Science at Reykjavík University, my own stamping ground, is seeking a new dean. Our present dean, Ari K. Jónsson, will take over the rectorship of the university on January 23, 2010, and we are looking for excellent candidates to take over the deanship of the school. (The dean has direct responsibility for academic, administrative and fiscal operations of the School of Computer Science. The dean is part of the executive committee of the university and reports directly to the rector.)


The School of Computer Science hosts several active research groups and its main research areas are artificial intelligence, combinatorics, databases, human-computer interaction, natural language processing, software engineering, theoretical computer science and virtual environments.
 

The job announcement is here. Is any of you out there interested in applying for the job?

A Question on the Structure of Fields, Centres and Committees

Can anyone briefly explain to me, or point me to on-line information about, the raison d'être and operating characteristics of structures like the fields and centres at Cornell and MIT, or the interdisciplinary committees found at the University of Chicago?

I am asking wearing my hat of the chairman of the research council of my university, where we are mulling about the possibility of having similar structures. Thanks in advance for any information you might be able to provide!

Tony Hoare on Industrial vs. Pure Research

I have just read a very cogent retrospective piece that Tony Hoare has written for the October 2009 issue of CACM to mark the 40th anniversary of the publication of his seminal paper An axiomatic basis for computer programming. (This is the first article he wrote as an academic. Not a bad way to start, is it?) It is a read that I thoroughly recommend and that I'll make available to the students who are now taking my course on the semantics of programming languages. I am posting an excerpt from that viewpoint article on industrial vs. pure research in computer science since it may be of interest to readers of this blog. I pass the word to Tony.

"Pure academic research and applied industrial research are complementary, and should be pursued concurrently and in collaboration. The goal of industrial research is (and should always be) to pluck the 'low-hanging fruit'; that is, to solve the easiest parts of the most prevalent problems, in the particular circumstances of here and now. But the goal of the pure research scientist is exactly the opposite: it is to construct the most general theories, covering the widest possible range of phenomena, and to seek certainty of knowledge that will endure for future generations. It is to avoid the compromises so essential to engineering, and to seek ideals like accuracy of measurement, purity of materials, and correctness of programs, far beyond the current perceived needs of industry or popularity in the market-place. For this reason, it is only scientific research that can prepare mankind for the unknown unknowns of the forever uncertain future.

So I believe there is now a better scope than ever for pure research in computer science. The research must be motivated by curiosity about the fundamental principles of computer programming, and the desire to answer the basic questions common to all branches of science: what does this program do; how does it work; why does it work; and what is the evidence for believing the answers to all these questions? We know in principle how to answer them. It is the specifications that describe what a program does; it is assertions and other internal interface contracts between component modules that explain how it works; it is programming language semantics that explains why it works; and it is mathematical and logical proof, nowadays constructed and checked by computer, that ensures mutual consistency of specifications, interfaces, programs, and their implementations. There are grounds for hope that progress in basic research will be much faster than in the early days. I have already described the vastly broader theories that have been proposed to understand the concepts of modern programming. I have welcomed the enormous increase in the power of automated tools for proof. The remaining opportunity and obligation for the scientist is to conduct convincing experiments, to check whether the tools, and the theories on which they are based, are adequate to cover the vast range of programs, design patterns, languages, and applications of today's computers. Such experiments will often be the rational reengineering of existing realistic applications. Experience gained in the experiments is expected to lead to revisions and improvements in the tools, and in the theories on which the tools were based. Scientific rivalry between experimenters and between tool builders can thereby lead to an exponential growth in the capabilities of the tools and their fitness to purpose. The knowledge and understanding gained in worldwide long-term research will guide the evolution of sophisticated design automation tools for software, to match the design automation tools routinely available to engineers of other disciplines."

Amir Pnueli Dies

I just learned via a posting on the TYPES mailing list the sad news that Amir Pnueli, one of the inspirational and leading figures in several areas related to the formal specification and verification of computing systems, passed away yesterday at age 68. An email message circulated yesterday by his family states that "Amir has suffered a serious brain hemorrhage which he could not recover from. He passed away today [2 November] at noon."

In 1996, Pnueli received the Turing Award for seminal work introducing temporal logic into computing science and for outstanding contributions to program and systems verification.

His scientific legacy will be felt for many years to come.

Benchmarking Metrics: What and Why?

In his post entitled "Top 10 theory schools?", Jonathan Katz gives a list of what he considers to be the top 10 theory departments in the US. (Read the post and the comments for an update on the discussion.) One of the comments reads as follows:

I would agree about:


MIT (Silvio, Shafi, Ron, Michel, …)
Cornell (Rafael, Eva, Jon, Bobby,…)
Berkeley (Luca, Christos, Umesh,…)
CMU (Venkat, Manuel, Avrim, Ryan,…)
Princeton (Boaz, Sanjeev, Moses, Bernard,..)

The others are a bit flakier:

GA Tech (Santosh, Chris, Vijay, Sasha, …)
UT Austin (Adam, David, Brent)
UCSD (Mihir, 1/4 Russell, Daniele, maybe Hovav)
U Washington (Anna, Paul, Anup)

I would say at least he following schools are VERY comparable to above:

Stamford (Dan, Serge, Tim, Amin,…)
NYU (Subhash, Assaf, Yevgeniy, Richard, …)
Harvard (Salil, Michael(s), Leslie)
Columbia (Mihalis, Rocco, Tal)

I would say there are top 5, and then top 10 following them.

So this commentator measures the quality of a theory group using the perceived research quality of the very best researchers at a given institution. Another possible metric would be the size of the group of active researchers with high international visibility. Yet others could be the number of peer-reviewed publications in top-class journals and conferences, or the average such number per staff member.

What criteria are most useful and why (bearing in mind that, at the end of the day, we are always making subjective judgements)? I am interested in this topic since the School of Computer Science I am working at is presently undertaking a benchmarking exercise. The aim of the exercise is to find three to four departments in the Nordic countries with which we aim at comparing ourselves in the very short term, within five years and within 10-15 years. One of the interesting aspects of this exercise is that our school is substantially smaller than most of the departments elsewhere. So, what do you think would be good metrics for the benchmarking exercise? Standing of the top scientists within the school? Average number of peer-reviewed publications and citations? Or what?

EATCS Award 2010: Call for Nominations

The Call for Nominations for the EATCS Award 2010 has been published (see this pdf). Nominations and supporting data should be sent to the chairman of the EATCS Awards Committee, Emo Welzl. The next award is to be presented during ICALP'2010 in Bordeaux. The deadline for nominations is: December 15, 2009. So get your act together quickly and nominate one of the many "obvious suspects" for the award! 

Note that nominations are now kept alive for three years. Since I sent in an unsuccessful nomination last year, I don't need to do anything this time around and will just be a very interested observer :-)


I wish the award committee the best of luck with their work.

Five Years of Logical Methods in Computer Science

I have received this letter via email. I post it here since I strongly support journals like LMCS and I encourage my readers to submit good papers to it. Happy birthday LMCS! May your reputation grow with the years.



Dear Colleague:

We would like to bring the community up to date on the journal

   Logical Methods in Computer Science
   www.lmcs-online.org

We started this fully refereed, open access, free electronic journal in January 2005, intending to create a high-level platform for publications in all theoretical and practical areas in computer science involving logical methods, taken in a broad sense. We are now on Issue 3 of Volume 5 (there are four issues a year). So far, we have received more than 350 submissions of which we have published 162. In addition to individual submissions, our journal publishes special issues, e.g., of selected papers of high-level international conferences such as LICS, IJCAR, CAV, CSL, and RTA.

We are continuing actively to develop the journal. For example, we accept survey articles, and are developing `live' surveys, which can be continually updated as knowledge progresses. In another direction, we are considering allowing authors to provide additional material of an expository nature, such as slides and videos, to enable them to interest a wider spectrum of readers in their contribution.

The journal is an overlay of CoRR, the computer science repository of arXiv. There are no fees for authors nor for readers. Every paper is refereed by two or more referees, and high standards are applied. The editorial board consists of about sixty top specialists in all areas of logic in computer science.

The journal is covered by Mathematical Reviews, the ISI Web of Knowledge, and the DBLP Database.

We welcome your comments and suggestions, and we seek your contributions! For more information please consult our web pages:

     www.lmcs-online.org

Yours,

Editor-in-Chief:   Dana S. Scott <dana.scott@cs.cmu.edu>
Managing Editors:  Benjamin C. Pierce <bcpierce@cis.upenn.edu>
                  Gordon D. Plotkin <gdp@inf.ed.ac.uk>
                  Moshe Y. Vardi <vardi@cs.rice.edu>
Executive Editors: Jiri Adamek <adamek@iti.cs.tu-bs.de>
                  Stefan Milius  <s.milius@tu-bs.de>

IFIP 1.8 workshop on FORMAL METHODS FOR EMBEDDED SYSTEMS

I have received the following announcement from Bas Luttik. I am happy to post it here since the event will be of interest to concurrency theorists and people working on formal methods at large, many of whom will be in Eindhoven for FM week.  (Not to mention the fact that I am the outgoing chair of IFIP WG 1.8.)

==============================

========================================
                       CALL FOR PARTICIPATION
======================================================================
      IFIP 1.8 workshop on FORMAL METHODS FOR EMBEDDED SYSTEMS

               http://www.cse.unsw.edu.au/~rvg/FMES/

           Eindhoven, The Netherlands, November 5, 2009
======================================================================

This IFIP 1.8 workshop is organised as part of the Formal Methods Week,
which takes place in Eindhoven from November 2 until November 6, 2009.
The goal of the workshop is to summarise research from different areas
of formal methods targeted to embedded systems, and to promote the use
of formal methods in different applications and in the engineering
discipline for embedded systems.

PROGRAMME:
----------
 8:30  Registration and coffee
 8:50  Opening

 9:00  Bert van Beek -
         The Compositional Interchange Format: concepts, formal basis,
         and applications
 9:45  Holger Hermanns -
         Synchronous vs. Asynchronous Performance Models of Industrial
         Networks on Chip Designs

 10:30 Coffee break

 11:00 Catuscia Palamidessi -
         Synchronization in the pi-calculus
 11:45 Joost-Pieter Katoen -
         Analysis and Semantics of Extended AADL Models

 12:30 Lunch
 14:00 The End

For abstracts of the talks and further details about the workshop we
refer to http://www.cse.unsw.edu.au/~rvg/FMES/.

REGISTRATION
------------
The registration fee for the workshop is 45 euros and covers coffee/tea
and lunch. You also need to register for FMweek, which costs an
additional 35 euros (administration costs). Please register via the
FMweek website: http://www.win.tue.nl/fmweek

WORKSHOP ORGANISERS:
---------------------
Rob van Glabbeek (National ICT Australia)
Ursula Goltz (Technical University Braunschweig, Germany)
Bas Luttik (Technische Universiteit Eindhoven, The Netherlands)
Uwe Nestmann (Technical University Berlin, Germany)

Presburger Award

In an old post I announced that the EATCS was about to initiate a young researcher award. I am happy to see that the call for nominations for the first Presburger Award has now been advertised. See here for the details. The award is meant for scientists in TCS who are 35 or younger.

The award is named after Mojzesz Presburger who accomplished his ground-breaking work on decidability of the theory of addition (which today is called Presburger arithmetic) as a student in 1929.

The award includes an amount of 1000 € and an invitation to ICALP 2010 for a lecture.

I hope you will take the time to nominate young scientists for the award. Who would be your favourite candidates?

Treatment of Alan Turing was “appalling”

Arnar Birgisson, a former MSc student of mine who is now a PhD student at Chalmers, pointed out to me that last Thursday Gordon Brown issued a statement "recognising the “appalling” way he [Alan Turing] was treated for being gay." The piece of news may be found here.

It is understandable that Gordon Brown's statement focuses on Turing's work on breaking the German Enigma codes. However, I find it suprising that Turing's role in the development of computer science does not deserve any mention at all in the apology.

The statement ends as follows:

"So on behalf of the British government, and all those who live freely thanks to Alan’s work I am very proud to say: we’re sorry, you deserved so much better."

So long, and thanks for breaking the Enigma code, devising the Turing machine and the universal Turing machine, building some of the earliest programmable computers and all the rest.....

Nominations for the Gödel Prize 2010

The Call for Nominations for the 2010 Gödel Prize has been posted (see this pdf file). The 2010 Award Committee consists of Cynthia Dwork (Microsoft Research), Johan Håstad (KTH Stockholm), Jean-Pierre Jouannaud (INRIA and Tsinghua University; chair), Mogens Nielsen (University of Aarhus), Mike Paterson (University of Warwick) and Eli Upfal (Brown University). The deadline for nominations is 31 January, 2010.

I hope that the volume B community will nominate some excellent papers to give the very strong volume A papers a run for their money :-) What papers would you nominate? Post a comment with your favourite candidates. Perhaps you can garner some support for them, leading to an actual nomination for the prize.

I will try to post some suggestions myself when my list of things to do shrinks to an acceptable level. (Fat chance, alas.)

Tom Henzinger: The First President of IST Austria

Last Sunday night I came back to Iceland after a thoroughly enjoyable stay in Bologna for CONCUR 2009, SOS 2009 and the 16th EXPRESS workshop. This was a welcome opportunity to see many friends and colleagues, letting alone visiting my home country and a pretty city like Bologna.

I hope to find some time to report on the conference, not least to pay tribute to the great work done by the local organizers and their team (with special thanks to Christian, Cinzia, Ferdinanda, Jacopo and Jorge). With the start of the teaching period approaching fast and a pile of chores to catch up on, here I'll just limit myself to mentioning a piece of news that I learned at the conference while discussing with Krishnendu Chatterjee. From 1 September, Tom Henzinger is the first President of the Institute of Science and Technology (IST) Austria in Klosterbeuburg. You can read the official press release here.

The aim of the institute, which is richly funded by the Austrian government, is "to become a world-class research center offering, by 2016, an international, state-of-the-art environment for approx. 500 scientists and doctoral students." This commitment to excellence and to basic research is witnessed already by the first few hires IST has made and things can only improve under Tom's presidentship.

I wish Tom and IST the best of luck. It is great to see Austria invest on basic research with the creation of such an institute, which is already bringing to Europe top-class scientists like Herbert Edelsbrunner (the only computer scientist to have won the National Science Foundation's Alan T. Waterman Award) and researchers of exceptional promise like Krishnendu. Moreover, it is really awesome to see one of us be chosen as the leader of such an institute.

In Bologna I also guessed correctly that Tom is the scientist with the largest number of papers during the first 20 years of CONCUR (21 papers overall). I have every reason to believe that Tom Henzinger will continue to contribute to research in concurrency theory even as president of IST.

CAV Award 2009

Does any of my readers know who received the 2009 CAV Award? The conference ended on July 2, but the web page has not been updated with that information.

Post a comment if you know who the recipient of the award was.

A Look at my Crystal Ball

Let me make an attempt at predicting the winner(s) of the LICS Test-of-Time Award for 2009.

According to the rules of the award, the prize will go to a paper that was presented at LICS 1989 in lovely Asilomar. I was there as a second-year Ph.D. student and I presented a paper myself, but it was not award material.

The conference programme was really good and the award committee must have had a difficult choice. I do not know who will receive the award in mid-August, but let make a personal prediction: the award will be shared by the following two papers:

• Douglas J. Howe, Equality in lazy computation systems and
• Eugenio Moggi, Computational lambda-calculus and monads.

What papers do you think will receive the award? It will be interesting to look back at the predictions and see who was right.

Arthur Benjamin's Proposal for Changing Maths Education

ICE-TCS Theory Day 2009

Last Friday, ICE-TCS hosted its fifth annual theory day. This is an event we organize each year to advertise TCS to the local scientists and students, usually in connection with visits by guests of the centre from outside Iceland. (The list of previous guest speakers includes Thomas Erlebach, Wan Fokkink, Ryan Hayward, Jan Kratochvil, Kim G. Larsen, MohammadReza Mousavi, Mogens Nielsen and Moshe Vardi.)

The programme for this year's event is here. We had a keynote address delivered by Zoltan Esik, who presented work on regular words and linear orders, which may be found in, e.g., this paper of his. The session devoted to algorithms saw two excellent talks by the Halldórsson brothers on algorithms for detecting genomic copy variations and on scheduling wireless networks. (The latter talk was based on a paper that will be presented at ICALP 2009.) The scientific programme was brought to a close by two talks by PhD students, who are the future of TCS. Paul van Tilburg (Eindhoven University of Technology, NL) described some of the results he has achieved in his research work so far, which aims at connecting the time-honoured theory of automata with the theory of processes. Matteo Cimini (a PhD student I am supervising with Anna Ingolfsdottir) explained the Curry-Howard isomorphism, which is one of the pearls of TCS, to all of us in a clear way.

The event was followed by wine, pizza and a social gathering. The only happening that marred our celebration of TCS is a 6% salary cut that was announced by our rector during the session in the programme devoted to algorithms.

"May you live in interesting times" says an old Chinese curse. These are definitely interesting times here in Iceland, alas. However, despite the lack of resources, ICE-TCS will try to keep waving the flag of TCS on the island as far as it can. If you happen to be in Iceland and you wish to drop by and give a talk in our seminar series, drop us a line.

Concurrency column for the June 2009 issue of the BEATCS

Last month I submitted the concurrency column for the June 2009 issue of the BEATCS to the editor in chief. The piece is entitled Deriving labelled transition systems --- a structural approach and has been contributed by Julian Rathke and Pawel Sobocinski.

The paper reports on recent results obtained by the authors in their ongoing research effort whose aim is to contribute to the development of a general theory for the systematic derivation of a labelled transition semantics for a process calculus from a simpler, non-structural, description of the reduction semantics.

I think that we can expect to hear further developments on this line of work soon, but the authors already have a good story to tell and the paper they contributed to the BEATCS witnesses this fact.

Thanks to Julian and Pawel for their efforts in putting this good paper together!

Announcing LIPIcs, a new series of electronic conference proceedings in computer science

I just saw the appended message on the concurrency mailing list. I think that it will be of interest to readers of this blog. Much is afoot in the area of open-access conference and workshop proceedings and I guess that several events will consider publishing their proceedings in this series.

----

Dear colleagues,

Following an initiative of the conferences STACS (http://stacs-conf.org) and FSTTCS (http://www.fsttcs.org/), to opt for non-commercial, electronic proceedings, the German conference center Schloss Dagstuhl Leibniz Center for Informatics (LCI) has decided to establish a new series of conference proceedings called Leibniz International Proceedings in Informatics (LIPIcs,http://www.dagstuhl.de/en/publications/lipics/). The objective of this series is to publish the proceedings of high-quality conferences in all fields of computer science. An Editorial Board is being instituted to oversee the selection of the conferences to be included in this series.

Details about joining this serie and about the editorial process can be found on-line, http://www.dagstuhl.de/fileadmin/redaktion/DROPS/LIPIcs/lipics_announce.pdf. The main features are as follows:
The proceedings in the LIPIcs series will be published electronically and will be accessible freely and universally on the internet, keeping the copyrights with the authors, and under an open access license guaranteeing free dissemination. To face the cost of electronic publication, a one-time fee will be required from the conference organizers. This fee will be kept to a minimum, intended to cover the costs of LCI, thanks in particular to a sharing of the workload between LCI and the conference organizers.

The LCI and the LIPIcs Editorial Board wish to attract the best conferences in computer science, and they hope you can encourage steering and program committees to join it!

Pascal Weil
LaBRI - CNRS
351 cours de la Libération
33405 Talence Cedex - France

pascal.weil@labri.fr
http://www.labri.fr/~weil

EPTCS, a new open access proceedings series

I have received the following message from Rob van Glabbeek, which I am very happy to post on this blog. I encourage readers of this blog to spread the announcement at their own institutions and to post it on their blogs, if they have any. I like to think that this new series of open access proceedings will offer the TCS community a good service. Of course, only time will tell whether this will happen, but I feel that the time is ripe for such initiatives in the TCS community. Spread the news!

With this posting, we are launching

   Electronic Proceedings in Theoretic Computer Science (EPTCS)

a new international refereed open access venue for the rapid
electronic publication of the proceedings of workshops and
conferences, and of festschrifts, etc, in the general area of
theoretical computer science, broadly construed.

We do not charge authors or event organisers for electronic
publication in EPTCS in any way. If hard-copies of proceedings are
desired, event organisers have the choice of organising the printing
themselves or taking advantage of a standard contract we will make
with a printing house. Copyright on all papers is retained by the
author, and full-text electronic access to all papers is freely
available, without any need for registration or subscription.

Permanent archival of EPTCS publications is ensured by organising
EPTCS as an overlay of the Computing Research Repository (CoRR): see
arXiv.org. The content of EPTCS will be indexed by DBLP.

Only original papers will be considered for publication in EPTCS:
manuscripts are accepted for review by an EPTCS conference or workshop
with the understanding that the same work has not been published, nor
is presently submitted, elsewhere. However, full versions of extended
abstracts published in EPTCS, or substantial revisions, may later be
published elsewhere.

The submission and refereeing process is handled entirely by the
organisation of the conference, workshop or festschrift to which the
paper is submitted. Our editorial board carefully selects which
workshops and conferences can be trusted to select scientific papers
of quality only, and only those events will be granted a contract to
fill a volume of EPTCS.

Our editorial board consists of:

Luca Aceto  Rob van Glabbeek Gordon Plotkin  
Rajeev Alur  Lane A. Hemaspaandra Vladimiro Sassone 
Krzysztof R. Apt Matthew Hennessy Robert H. Sloan  
Lars Arge  Bartek Klin  Wolfgang Thomas  
Ran Canetti   Evangelos Kranakis Irek Ulidowski  
Luca Cardelli  Shay Kutten  Dorothea Wagner  
Rocco De Nicola  Nancy Lynch  Martin Wirsing  
Jose' Luiz Fiadeiro Aart Middeldorp  Moti Yung  
Wan Fokkink  Benjamin Pierce     

Further information can be found on our website:

     http://eptcs.org/.

In the hope this initiative will benefit the theoretical computer
science community,

Rob van Glabbeek
(Editor in Chief)

Accepted Papers for LICS 2009

The list of papers selected for presentation at LICS 2009 is out. At first sight, it wasn't a great year for concurrency theory, but the programme looks very interesting as usual. Some of the papers I intend to check out when I can get my hands on them, and the dust settles, are, e.g.:

• Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Joachim Parrow, Magnus Johansson, Björn Victor and Jesper Bengtson. Psi-calculi: Mobile processes, nominal data, and logic
• Frank Pfenning and Robert Simmons. Substructural Operational Semantics as Ordered Logic Programming
• Sumit Nain and Moshe Vardi. Trace Semantics Is Fully Abstract
• Udi Boker and Orna Kupferman. Co-ing Büchi: Less Open, Much More Practical

Plenty to read! Congrats to Sumit and Taolue, with whom I have had the pleasure to co-author papers at some point in the past.

Abel Prize 2009 to Gromov

The IMU electronic newsletter has informed me that The Norwegian Academy of Science and Letters has decided to award the Abel Prize for 2009 to Mikhail Leonidovich Gromov for "his revolutionary contributions to geometry". As his Wikipedia page clearly indicates, Gromov has received a host of other awards before.

Reading material on Gromov and his work is available here. Being unable to understand his technical work, I will limit myself to pointing out what people have said about him.

• "It is incredible what Mikhail Gromov can do, just with the triangle inequality." (Dennis Sullivan)
• "The works of Mikhail Gromov should be read until the pages fall off." (Marcel Berger)

I would be happy if anyone apart from my coauthors and I ever read any of the my papers once, let alone "until the pages fall off".

Here is what the great man says about his opus:

The readers of my papers look only at corollaries, sometimes also at the technical tools of the proofs, but almost always never study them deeply enough in order to understand the underlying thought.

Does this mean that the "underlying thought" is carefully hidden in Gromov's papers? Shouldn't it be one of the author's duties in writing a paper to make the underlying thought apparent to the readers? What useful role can hiding the author's thoughts from the readers possibly have?

Anyway, we are surely in the presence of a giant of human thought, so kudos to him from a (hopefully) honest toiler.

Introduction to CS

Today I attended a curriculum revision meeting at my school. In particular, two new courses were discussed, and I feel that their quality will be paramount to the possible success of the revision effort. The courses are Introduction to CS and Problem Solving. The aim of the former course is to introduce incoming students to the algorithmic way of thinking and its applications in CS, as well as to introduce them to basic programming skills. Historical remarks on, and context for, the material covered in the course will be given to put it into perspective.

Can any of my readers point out suitable textbooks for such a course and/or examples of courses you are familiar with that have a similar emphasis?

Any experience report on problem solving courses would also be most welcome. Thanks in advance!

ACM TOCL Seeks New Editor in Chief

I have received this announcement from Vladimiro Sassone (chairman of the steering committee for the ETAPS conference series), who received it from Joe Halpern. I am posting it here since it may be of interest to readers of this blog.

Nominations (including self nominations) are invited for the next Editor-in-Chief of ACM Transactions on Computational Logic (ToCL):

http://www.acm.org/pubs/tocl/.

The position is for a term (renewable once) of three years, starting on July 1, 2009.

Candidates should be well-established researchers in areas related to computational logic, broadly conceived, and should have sufficient experience serving on conference program committees and journal editorial boards. Nominations, including a current curriculum vita and a brief (one page) statement of vision for ToCL, should be sent to Joseph Halpern <halpern@cs.cornell.edu>, by May 1, 2009.

Final selection will be made by a Selection Committee, consisting of Joseph Halpern (chair -- Cornell University), Kryzsztof Apt (CWI), Prakash Panangaden (McGill University), and Gordon Plotkin (University of Edinburgh). Nominations received after May 1, 2009, will be considered up until the position is filled.

Thanks for your help,

Joe Halpern

Ed Brinksma Becomes Rector of the University of Twente

I recently saw this press release (in Dutch) to the effect that Boudewijn Haverkort has become the new director of the Embedded Systems Institute in Eindhoven. Congratulations to him for this appointment.

By browsing through the press release, I learned that from January 1, 2009, Ed Brinksma, the former director of ESI, is Rector Magnificus of the University of Twente. Congrats to Ed too!

Ed is the second (theoretical) computer scientist I know of who has become rector of a European university. The other is Furio Honsell, the first ever computer scientist to become rector of an Italian university.

Do you know of other (theoretical) computer scientists who are rectors of universities? And is it good for the (T)CS community that some of its members take up rectorships? I do think so, and for many reasons mostly related to academic politics, but I'd like to hear your opinion.

A Socratic Dialogue on Theoretical Computer Science

The following piece will appear in a brochure aimed at future (post)graduate students that will be published by my university very soon. I am posting it here in case it may be of interest/use to any of the readers of this blog, and hoping that it won't hurt the cause of TCS too much. I was actually quite surprised that the PR office from my university did not send the piece back to me asking for a complete rewrite :-)

-----------------------

A Socratic Dialogue on Theoretical Computer Science

This dialogue takes place between 23:00 and 24:00 at the counter of the bar in a trendy night club. Alice and Bob have just met and they are sipping a glass of wine. The ice has already been broken and they try to find out more about each other.

Bob: I am a physicist. What do you do?
Alice: I am a computer scientist.

Bob: You are the first woman computer scientist I have met! There aren't many women who like to program or fix computers for a living, aren't there?

Alice: Well, actually I am a theoretical computer scientist.
Bob: (Not hiding a look of surprise on his face.) You must be joking! This surely is a contradiction in terms. There is little that is as practical as, and less theoretical than, computer science! Pardon me for saying so, but, as a scientist myself, I have some level of familiarity with computers, and I know from my daily experience that these machines have dramatically changed many aspects of my work and of my life. I really could not live without my iPod!

I have also read that what we are witnessing today is just the beginning of a digital revolution and that a population of 'effectively invisible' computers around us is embedded in the fabric of our homes, shops, vehicles, farms and some even in our bodies. However, computing is just a technology, not a science.
Alice: (With a smile on her face and sipping her wine.) You are not alone in thinking so. However, the information-technology revolution is a glaring example of how results from basic scientific research, having its roots in subjects such as mathematical logic and computability theory, which once looked very abstract and remote from actual application, lead to technological innovations that cause far-reaching transformations to our society. Because of computer science, logic is the most applied branch of mathematics today.
Bob: I am not easily convinced. What is Theoretical Computer Science (TCS)?
Alice: Let me rest on the shoulders of giants and quote Oded Goldreich and Avi Wigderson, two of the foremost (theoretical) computer scientists of our time:

TCS is the fundamental scientific discipline that aims at understanding general properties of computing, be it natural, man-made, or imaginary.

In fact, in some sense, the whole world of computing arose from Alan Turing's analysis of an imaginary computing device (the Turing machines you might have heard of) that he invented in order to understand the notion of mechanical computation. That imaginary device eventually gave birth to the computers of today and to the software that drives them. So computers arose as the answer to man's quest to understand computation, something that is around us in nature and in our artifacts.
Bob: Yes, I am aware that Nature itself "computes". It is not uncommon these days to see theoretical physicists discuss the information content of black holes or of the universe itself, or the feasibility and power of quantum computation or other computing principles from the physical world. But tell me, how do theoretical computer scientists work? What contributions has the field given to science?

Alice: (Her face becoming brighter with joy.) Research in TCS often starts from the desire to understand the properties of some notion of computation. In particular, we are interested in characterizing what algorithmic problems can be solved, in theory or in practice, using the chosen notion of computation. You know, computers look very powerful, and indeed they are. (Bob nods.) However, they are not omnipotent and there are many precisely formulated problems that they will never be able to solve. Characterizing the notion of computational process and showing the existence of unsolvable problems was one of the early breakthroughs of TCS around 1936, long before any computer existed! Since then, we have learned a lot about the notion of computational complexity of problems. Have you ever watched the TV show Numb3rs?

Bob: (Smiling) Sure, there is a cool physicist in it who walks around with Charlie Eppes.
Alice: (Smiling back) Good. Then you might recall that Charlie Eppes every now and again tries to solve the "P vs NP" problem. This is a problem from computer science that is one of the most fundamental mathematical problems of our time. It is one of the Millennium Problems of the Clay Mathematics Institute (in fact, it is the first such problem) and is the only one amongst them that, apart from its intrinsic scientific interest, has profound practical applications and even philosophical implications!
Bob: (Taken aback) What does that problem have to do with philosophy?
Alice: (Sensing victory) Well, there is a strong sense in which the solution of that problem would allow us to automate efficiently the creative process of finding solutions to a plethora of computational problems in many areas of science. Some people like to say that the "P vs NP" problem can be rephrased as asking whether creativity can be efficiently automated. People in my community tend to believe that the answer is no and that some computational problems are intrinsically hard to solve. Do you shop on line?
Bob: Sure I do, just like anyone else.
Alice: In fact, every time you submit your credit card number for an on-line purchase, you are implicitly trusting that a very basic mathematical problem, the time-honoured decomposition of a number into its prime factors, is computationally hard. The whole of cryptography is a very active branch of TCS.
Bob: Now you really have to tell me more. What are the typical questions people like you work on?
Alice: I am glad you asked, but I do not want to bore you too much.
Bob: (Laughing) Well the night is still young, and I feel that we are on the same wavelength. So, go ahead.
Alice: Well, some of my colleagues still work on understanding what can be possibly computed in principle or with certain bounds on the amount of the resources at our disposal. You know, some problems can in principle be solved using a computer, but in practice this would require more time than the age of the universe. Others develop increasingly sophisticated algorithms for solving computational problems. These are the algorithms that, for instance, allow you to search for a lot of the information you need using Google in less than no time, schedule many of the aspects of the daily life of our city as well as the timetable of the classes that we took at university. Do you drive a car?
Bob: Sure, but not tonight. (Laughs)
Alice: Well, the functioning of many of your car's features relies on the algorithms these colleagues of mine develop as well as on the analysis techniques that others have proposed for making models of the behaviour of the ABS system in your car, say, for describing its expected properties and for checking that the system affords the properties on your wish list. You do expect your car's airbag to inflate immediately after a crash, do you? (Alice smiles.)
Bob: Sure I do! (He smiles back.)
Alice: Then it's on the work of people like me your trust is based. And we haven't even started talking about computational learning theory, information theory, global computing and the design of the internet markets you use and inhabit. Did you know that thanks to innovations in learning theory developed by theoretical computer scientists automated search and data selection methods have become indispensable in a growing number of fields including yours? Computers can "learn"! And I have not yet told you about the theory of programming languages and the study of methods for describing what programs do when they compute.....

Bob: I think I need a little fresh air. Let's get out of here and take a walk. I am ready to hear your stories, but not in this noisy place.

Alice and Bob collect their jackets and head out. A full moon was lighting the sky and heard Alice ask: "Do you know that coding theory allows us to perform error-free transmission of information to and fro the spacecrafts that we send out to explore the solar system and beyond? Coding theory is also a very active area of TCS...."

February 2009 Issue of the BEATCS

The February 2009 issue of the Bulletin of the EATCS is now available, and is freely accessible to anyone interested in perusing it---as it should be for the bulletin of any professional organization whose aim is to further the development of its scientific area.

This issue of the Bulletin features the first contribution to a brand new column, The Algorithmic Game Theory Column, edited by Marios Mavronikolas. In a Greek relay team, Panagiota Fatourou takes over from him as the new editor of the Column on Distributed Computing, whose latest instalment is devoted to a piece on the theory of transactional memory.

There is much to read and enjoy, as usual. Readers might notice, however, that the Concurrency Column is missing. Mea culpa....

An Opinion Poll Related to the Bulletin of the EATCS

I append a questionnaire that I have helped put together in my role as chairman of the publication committee of the European Association for Theoretical Computer Science. The questionnaire will be sent out to all the past and present members (so some of you will receive it via email soon), but I'd also like to have the opinion of people in TCS who have never been members of the association. So, if you have time and/or interest in this matter, I'd be happy to receive a filled questionnaire from you or simply your answers to some of the questions. Use the comments section for submitting your input.

In case you wish to have a closer look, the Bulletin is freely available from this web page.

Let me remind you that people who registered for ICALP 2008 become members of the European Association for Theoretical Computer Science for a year. Becoming a member of the association is easy and cheap. See here.

--------------------------- QUESTIONNAIRE ------------------------



PART I: QUESTIONS RELATED TO THE POSSIBLE FUTURE DEVELOPMENTS OF THE BULLETIN OF THE EATCS

Note to the readers: Throughout the questionnaire BEATCS abbreviates Bulletin of the EATCS. Please return your answers in the comments section.
If you are already a member of the EATCS you will receive a copy of this questionnaire via email.

1. Do you think that the quality of the Bulletin of the EATCS (henceforth, BEATCS) has increased over the last five years? YES/NO/DON'T KNOW
1. If your answer is YES or NO, please state the reasons behind your answer.
Are you aware that the Bulletin of the EATCS is an open-access publication? YES/NO
1. If your answer is yes, how did you learn that the BEATCS is open access?
Do you think that the BEATCS should remain open access? YES/NO
Does the open-access status of the BEATCS influence whether you are a member of the EATCS? YES/NO
How often do you read the BEATCS? NEVER/ONE ISSUE per year/TWO ISSUES per year/ALWAYS
What parts of the BEATCS do you read?

2. What are your areas of scientific interest?
   
3. Do you think that the present contents of the BEATCS cater for the need of its readers and of the new generations of the TCS community as whole?
Is there any topic to which you think that the BEATCS should devote a new column?
4. If you are missing something in the BEATCS, what is it and what are your suggestions?
5. What do you think of the overall scientific quality of the columns in the BEATCS? VERY LOW/LOW/ACCEPTABLE/GOOD/VERY GOOD/EXCELLENT
Is there any column that you find particularly good?
1. In your opinion, is there any column whose quality needs to be improved substantially?
   
What do you think of the overall scientific quality of the contributed research articles? VERY LOW/LOW/ACCEPTABLE/GOOD/VERY GOOD/EXCELLENT
6. At present, the BEATCS has light reviewing for columns, in the sense that the column editor reviews contributions by guest columnists, and a rather informal reviewing of technical contributions by the Bulletin editor. Do you think that the BEATCS should strive to set up a more formal peer-review process for the contributions that are published as columns and/or for the technical contributions?
Do you think that the BEATCS should be indexed regularly by DBLP, ISI, and MathSciNet?

7. Should the BEATCS be transformed into a new journal-type publication with peer refereeing etc., and with most newsletter-style content transferred to the EATCS web site?
What could the BEATCS learn from publications like CACM and the Notices of the AMS?
To your mind, what is the flagship journal publication of the TCS community, i.e., the most representative journal mostly devoted to TCS?
8. To your mind, is the BEATCS suitable as the flagship publication of the EATCS?
9. To your mind, what is the most useful service that the BEATCS should provide to the TCS community?

PART II: ADDITIONAL QUESTIONS RELATED TO EATCS MEMBERSHIP

1. If you are a member of the EATCS, please state your main reasons for joining the organization.
If you are not a member of the EATCS, Please state your reasons for not joining the organization.
2. If you are missing something in the EATCS, what is it and what are your suggestions?

EATCS Award 2009 to Gérard Huet

The EATCS Award for 2009 will go to Gérard Huet. See the official announcement here. The Award will be assigned during a ceremony that will take place in Rhodes (Greece) during ICALP2009 (July 5-12, 2009).

The nomination singles out the following contributions by Huet.

• In the early 70's, Huet developed both resolution and unification for higher-order logic: these results have became the core of several modern systems that perform deduction in higher-order logic.
• Huet has done fundamental research in the areas of rewriting and Knuth-Bendix completion. His writings in this area are extensive and elegant. - Between 1982 and 1989, Huet directed and contributed to the design and implementation of the CAML functional programming language. That language and its descendants have given academics and industries an efficient and well structured programming language.
• In the 1990s, Huet and his students designed and built the first version of the Coq proof assistant. Today, Coq is one of the most used and trusted platforms for formalized mathematics and formal methods.

Congratulations to Huet and to French TCS, which has given and still gives important contributions to our field.

More Reading on Bibliometric Data

In a recent post, I advertised a critical note on the (ab)use of bibliometric data subscribed by all the members of the editorial board of the journal Mathematical Structures in Computer Science.

Similar concerns have been raised by others. See, e.g., the talk "Bibliometric Evaluation of Computer Science - Problems and Pitfalls" by Friedemann Mattern (Institute for Pervasive Computing, Department of Computer Science, ETH Zurich).

There is also a very interesting joint report from three mathematical boards, which is definitely worth reading.

Finally, the "Sector Overview Report from the Computer Science and Informatics Sub-Panel (UoA 23)" after the British nationwide "Research Assessment Exercise 2008" (available at http://www.rae.ac.uk) includes the following passage:

We frequently found that citation counts were poorly correlated with the sub-panel’s assessment of the impact of the work examined. Citations also varied widely between research areas. For instance, much of the highly significant theoretical research, in which the UK is world leading, typically attracts low citation counts. Despite these low citations, the work is often found to have profound long-term impact on practical aspects of the field.

(The emphasis is mine and is not present in the original text.)

I hope that some of you will find these contributions interesting. I thank Catuscia Palamidessi and Vladimiro Sassone for pointing them out to me.

A Couple of Papers on Structural Operational Semantics

begin rant

I like to think that I am not a procrastinator by nature and I try (but often fail) to apply Littlewood's zero-infinity law in my work, but am I the only one who feels that the number of things to do keeps increasing while the available time to carry them out decreases very fast?

end rant

One of the many things that I have been struggling to get done on time in this hectic early 2009 was a report on the first year for one of my ongoing grants. This reminded me of two papers I recently co-authored that I had meant to mention on this blog. Both papers offer a modest contribution to the meta-theory of Structural Operational Semantics.

Structural Operational Semantics (SOS) was introduced by Gordon Plotkin as a logical and structural approach to defining operational semantics for programming and specification languages. The logical structure of SOS specifications supports a variety of reasoning principles that can be used to prove properties of programs whose semantics is given using SOS. Moreover, SOS language specifications can be used for rapid prototyping of language designs and to provide experimental implementations of computer languages. Thanks to its intuitive appeal and flexibility, SOS has become the de facto standard for defining operational semantics, and a wealth of programming and executable specification languages have been given formal semantics using it.

The meta-theory of SOS provides powerful tools for proving semantic properties for programming and specification languages without investing too much time on the actual proofs; it offers syntactic templates for SOS rules, called rule formats, which guarantee semantic properties once the SOS rules conform to the templates (see, e.g., the papers in this bibliography maintained by MohammadReza Mousavi). In some sense, this is akin to an axiomatic development of the theory of operational semantics. One devises some rule patterns (the aforementioned rule formats) that "axiomatize" sufficient syntactic conditions guaranteeing that all programs in a language afford some desirable semantic property.

There are various rule formats in the literature for many different semantic properties, ranging from basic properties such as commutativity and associativity of operators, and congruence of behavioral equivalences to more technical and involved ones such as non-interference and (semi-)stochasticity.

The most recent paper I wanted to mention here is entitled Rule Formats for Determinism and Idempotency and is coauthored with Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. (An extended abstract of this work will appear in the Proceedings of Third FSEN: IPM International Conference on Fundamentals of Software Engineering (FSEN09), Iran, April 15-17 2009. Lecture Notes in Computer Science, Springer-Verlag, 2009.) In that paper, we propose rule formats for two properties, namely, determinism and idempotency of binary operators. In hindsight, it is quite surprising that no rule format guaranteeing determism had been proposed before. After all, determinism is a natural and important semantic property, which holds for sub-languages of many process calculi and programming languages, and is also a crucial property for many formalisms for the description of timed systems---where time transitions are required to be deterministic, because the passage of time should not resolve any choice.

Idempotency is a property of binary composition operators requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. Idempotency of a binary operator f is concisely expressed by the following algebraic equation.

f (x, x) = x

Determinism and idempotency may seem unrelated at first sight. However, it
turns out that, in order to obtain a rule format for idempotency that is sufficiently general to cover the special cases we wanted to cover, we need
to have the determinism of certain transition relations in place. Therefore, having a syntactic condition for determinism, apart from its intrinsic value, results in a powerful, yet purely syntactic framework for idempotency.

The second paper, On the Expressibility of Priority (Information Processing Letter 109(1):83-85, 2008), is joint work with Anna Ingolfsdottir. It is more modest in scope and offers results confirming that the priority operator of Baeten, Bergstra and Klop cannot be expressed using positive rule formats for operational semantics. Although expected, this inexpressibility result does not seem to have appeared before in the literature.

Overall, I really enjoyed working on those two papers. Thanks to my coauthors (old and new) for having given me the opportunity to work with them on these projects.

RAE 2008 Results

I just noticed that the results of the Research Assessment Exercise for 2008 are out. For Computer Science and Informatics, the league table may be found here. Cambridge tops the chart with Imperial College, Edinburgh and Southampton coming joint second. (In reading the ratings, bear in mind that 4* rating is defined as ‘world leading’ and 3* as ‘internationally excellent’.) You might also want to look at the detailed interpretation of the RAE results offered by Edinburgh, according to which Edinburgh is by far the strongest department in the UK.

All the aforementioned departments host very strong TCS groups.

The ranking for Pure Mathematics sees Cambridge land in fourth place, behind Imperial, Warwick and Oxford. Is this surprising? Honestly, I do not know.

The debate on the RAE is raging in the UK, and I guess that it will go on for some time.

A Critical Note on the Abuse of Bibliometric Data

This post is heavily based on an email message I received from Catuscia Palamidessi.

I have recently been informed by Catuscia Palamidessi that the editorial board of the journal Mathematical Structures in Computer Science has put together a critical note on the (ab)use of bibliometric data, which will appear in the issue 19.1 of that journal. The note has been written by the editor in chief, Giuseppe Longo, and subscribed by all the members of the editorial board of that journal.

The note expresses the worries of the scientists in the board about

• the way the evaluation of research activity is evolving in many countries,
  
• the general trend to use criteria purely based on numbers and citation indexes in judging the quality of researchers and
  
• the fact that the management of the data used in the numerical evaluations is entrusted to private agencies, whose methodologies and software might be rather dubious or cannot be subjected to scrutiny by the research community.

Did you know that

“The first journal according to ISI (...) is the 195th according to CiteSeer; the 2nd according to ISI does not appear in CiteSeer; the 6th for ISI is 958th for CiteSeer... Conversely, the 1st for CiteSeer (...) is 26th for ISI; the 4th for CiteSeer (...) is 122nd for ISI”

(See this document, in French.) I did not, and the fluctuation in the data is worrying, to say the least.

What is the situation regarding the use of citation indexes and impact factors in your country?

I hope that the readers of this blog will find the note interesting. It certainly gave me some food for thought. Feel free to distribute it as widely as you see fit.

Martín Abadi ACM Fellow 2008

I saw from this post that the list of ACM Fellows for 2008 is out. People in the research community I belong to, and in particular the other members of the IFIP WG on Concurrency Theory, will very pleased to see that Martín Abadi is on that list. Martín is honoured for "contributions to computer security and verification of computer systems."

Martín Abadi will be one of the invited speakers for CONCUR 2009.

Congrats to Martín and to all the other ACM fellows for 2008.