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.