EATCS Award 2016 to Dexter Kozen (Cornell University, USA)

The EATCS bestows the EATCS Award 2016 to Dexter Kozen (Cornell University, USA) for fundamental contributions across the whole spectrum of theoretical computer science

The EATCS is proud to announce that the EATCS Award Committee consisting of Fedor Fomin, Kim G. Larsen (chair) and Jean-Eric Pin has selected Dexter Kozen (Cornell University, USA; http://www.cs.cornell.edu/~kozen/)  as the recipient of the EATCS Award 2016.

Dexter Kozen is a theoretical computer scientist, perhaps the  theoretical computer scientist, who has excelled across the entire spectrum of our field and crashed through the so-called Volume A/Volume B barrier. Even within these tracks he has exhibited remarkable diversity and depth. This makes him an exceptional candidate for the EATCS Award and he continues the lineage of stellar scientists who have received the EATCS Career Award so far.

Dexter Kozen is known for his many contributions to theoretical computer science. These include, among many others, the most succinct and beautiful proof imaginable of completeness for PDL, a stunning treatment of the far more challenging mu-calculus and the elegant treatment of logics of programs in the setting of Kleene algebra. He has also made fundamental contributions to complexity theory. In fact, one of the first contributions of Dexter Kozen to the scientific community was the definition of the notion of alternating Turing machine, a deep contribution to complexity theory that made it possible to connect time and space complexity. The results were viewed as so significant that they almost immediately became part of the graduate curriculum in complexity theory. Dexter’s work on alternation appeared initially in his singly-authored FOCS’76 paper, independent of the Chandra-Stockmeyer paper that was published back-to-back with it in the same volume; the two later became the famous combined, very high-cited, triply-authored J.ACM version for which the authors won an IBM Outstanding Innovation Award in 1980.

Dexter Kozen’s work on modal logic and Kleene algebra has undoubtedly had a major impact in the area of programming logics and gathered a huge number of citations as it opened up this field.

Besides complexity theory and modal logic, Dexter Kozen also produced major results on algebra, such as the complexity of the theory of real closed algebraic theories, and on computer algebra, such as the Kozen-Landau theorem.

Dexter Kozen has also been a pioneer in probabilistic semantics. Long before it became fashionable, he worked on a measure-theoretic semantics  for probabilistic programs which remains the inspiration for the intense activity in topics like probabilistic programming languages, probabilistic process algebra and logics.

Dexter Kozen has had many collaborations. His connections to Amsterdam, Aarhus and Warsaw are probably the most well-known. He has spent several one year sabbaticals in Europe with successful collaborations. He is an inspiring person  and his presence in a department is of immeasurable value for young researchers. It is worth mentioning that Dexter Kozen’s support for the contacts with Eastern European colleagues has been admirable, at a time when this was rather difficult and complex to achieve.

David Harel's two-page  laudation that appears in the volume for Dexter's 60th birthday (available at http://www.wisdom.weizmann.ac.il/~harel/papers/Kozen.pdf) provides a wonderful introduction to Dexter Kozen as a scientist and as a colleague.

The  EATCS Award is given to acknowledge extensive and widely recognized contributions to theoretical computer science over a life-long scientific career. The list of the previous recipients of the EATCS Award is available at

http://eatcs.org/index.php/eatcs-award.

The EATCS Award carries a prize money of 1000 Euros and will be presented at ICALP 2016, which will take place in Rome (Italy) from the 12th till the 15th of July 2016.

Report on Dagstuhl Seminar 15511 on the Graph Isomorphism Problem (contribution by Anuj Dawar)

Anuj Dawar has kindly allowed me to post here his report on Dagstuhl Seminar 15511 on the Graph Isomorphism Problem, which will appear in the February 2016 issue of the Bulletin of the EATCS. IMHO, it is a real gem and conveys the excitement of the event wonderfully well. Enjoy it!

The February 2016 issue of the BEATCS will be brimming with interesting and though-provoking content, and will be open access as usual. I hope that you'll make a point of reading it, when it is published. Watch this space for further news on the issue.

Computer Science in Europe (contribution by Thomas A. Henzinger)

This is the second viewpoint piece I received in response to my call for opinions on the report on logic activities in Europe that Yuri Gurevich wrote in 1992. Thanks to Tom for taking the time to write this piece and for allowing me to share it on this blog. Enjoy it! 

Computer Science in Europe

Thomas A. Henzinger

IST Austria 

It saddens me but it would be difficult to refute a claim that, in the past two decades, Europe has been falling further behind the United States in the dynamism of the information technology industry, the popularity of the computer science major, and the impact of frontier research in computing. The vast majority of Turing awards still goes to researchers who work in the United States. It is particularly disconcerting that the main strengths of European computer science appear largely unchanged from 1994: on the academic side, Europe's research leaders are still concentrated disproportionately in formal methods, and on the industrial side, Europe's technology leaders are still found primarily in the "old" economy, exemplified by the automotive industry.

To close the gap, Europe desperately needs new organizational structures in academia, a greater entrepreneurial spirit of society, an improved image for computer science as a career choice, especially among women, the mandatory acquisition of computational thinking and coding skills in secondary education, and more emphasis on principles of systems building which are critical to industry in university curricula of computer science. Israel offers a role model for closing the gap with the United States with regard to the first three points ---academic structures, entrepreneurial culture, and the public image of computer science--- and has been a leader in computer science education.

There are a few encouraging signs of European computer science changing. The European systems community has begun to organize itself through efforts such as the Eurosys conference and some countries are trying to remedy their deficiencies in systems research. Germany, for example, founded the Max Planck Institute for SoftwareSystems. Several European countries and institutions have started to copy key aspects of the American career model, such as tenure tracks that give faculty early independence and doctoral programs that give students a broad graduate education. Student mobility and structured doctoral education are strongly supported by the Marie Curie program of the European Union and by the funding agencies of some countries, to counteract the wide-spread habit of researchers advancing in the same lab from undergraduate to faculty level.

There have been some remarkable institutional changes. EPFL has demonstrated that changes in the organization and recruiting can lead to dramatic improvements in the scientific reputation and attractiveness of an institution. Even entirely new institutions have been founded, such as IST Austria, which naturally find it easier to implement new structures such as a tenure track and an institutional doctoral school.

The most significant development can be found, perhaps surprisingly, on the European level. I am referring to the creation of the EuropeanResearch Council, which supports frontier research based purely on scientific criteria. This program has no counterpart in the United States, but if it manages to remain scientifically independent and well-funded, I am confident that its impact will change the game. These are big if's, of course, and the ERC is constantly being threatened by national interests and sectorial lobbies that favor traditional programs which distribute the available funds to more different countries, sectors, and groups. Given that politicians love to pride themselves with the founding of "strategic" consortia, centers, and flagships, and industry likes to get every possible cut of public money, the initial success of the ERC has been all the more remarkable. Let's work together so that it will trump the less effective funding formats and lift the strength of computer science in Europe.

On the Two Sides of the Atlantic in Logic and Computation (contribution by Moshe Y. Vardi)

Prompted by a reference to it in a recent CACM editorial by Moshe Vardi, I belatedly read the very interesting piece on logic activities in Europe that Yuri Gurevich wrote in 1992. I was struck by the idea that it might be interesting to ask some selected colleagues to contribute (short) opinion pieces to the Bulletin of the EATCS reflecting on the points raised by Yuri in that article twenty years later. 
In order to whet your appetite, I post below Moshe's contribution. Thanks to Moshe for taking the time to write this piece and for allowing me to share it on this blog. Enjoy it! 

On the Two Sides of the Atlantic in Logic and Computation

MosheY. Vardi

Rice University

In his 1977 EWD Note 611, “On the fact that the Atlantic Ocean has twosides,” Edsger Dijkstra noted the different attitudes towards computing research in Northern America and Western Europe. Yuri Gurevich noted the same phenomenon in his 1992 report, "Logic Activities inEurope." In a 2015 Communications of the ACM editorial I revisited this issue and asked “Why Doesn't ACM Have a SIG for Theoretical ComputerScience?^"

The key issue raised in that editorial was the split between Volume-A-type and Volume-B-type research in Theoretical Computer Science (TCS), referring to the 1990 Handbook of Theoretical Computer Science, with Jan van Leeuwen as editor. The handbook consisted of Volume A, focusing on algorithms and complexity, and Volume B, focusing on formal models and semantics. In other words, Volume A is the theory of algorithms, while Volume B is the theory of systems (hardware and software). North American TCS tends to be quite heavily focused on Volume A, while European TCS tends to encompass both Volume A and Volume B. The ACM Special Interest Group on Algorithms and Computation Theory (SIGACT) is, de facto, a special-interest group for Volume-A TCS.

I pointed out in my editorial that this division did not exist prior to the 1980s. In fact, the tables of contents of the proceedings of two North American premier TCS conferences—IEEE Symposium on Foundations of Computer Science (FOCS) and ACM Symposium on Theory of Computing (STOC)---from the 1970s reveal a surprisingly (from today's perspective) high level of Volume-B content. In the 1980s, the level of TCS activities in North America grew beyond the capacity of two annual single-track three-day conferences, which led to the launching of what was known then as "satellite conferences." Shedding the "satellite" topics allowed FOCS and STOC to specialize and develop a narrower focus on TCS. But this narrower focus in turn has influenced what is considered TCS in North America. In contrast, the European Association for Theoretical Computer Science (EATCS), expanded the scope of its flagship conference, the International Colloquium on Automata, Languages, and Programming (ICALP), by reorganizing the conference along several tracks. In 2015, ICALP consisted of three tracks: Track A: Algorithms, Complexity and Games; Track B: Logic, Semantics, Automata and Theory of Programming; and Track C: Foundations of Networked Computation: Models, Algorithms and Information Management. The reorganization along tracks allowed EATCS to broaden its scope, rather than narrow it like SIGACT.

But the reality is that if one zooms into Volume-B research, one finds again the Volume-A/Volume-B dichotomy, also reflected in the range of topics of the Symposium on Logic in Computer Science (LICS), the flagship conference of the ACM Special Interest Group on Logic and Computation (SIGLOG). Sub-volume A of Volume-B research is concerned with connections between logic, algorithms, and computational complexity. Descriptive-Complexity Theory, for example, aims at bridging computational complexity and logic by studying the expressive power needed to describe problems in given complexity classes. A celebrated result in this area is Fagin’s Theorem, which relates NP to Existential Second-Order Logic. Model Checking, as another example, studies the evaluation of logical formalisms, including various temporal logics, over finitely represented structures. Automata theory often provides tools to bridge between logic and algorithms. The Büchi-Elgot-Trakhtenbrot Theorem, for example, provides automata-theoretic tools for solving the satisfiability problem for Monadic Second-Order Logic on finite words.

Sub-volume B of Volume-B research, in contrast, is concerned with semantical and methodological foundations for programming and programming languages. Domain theory, for example, studies special kinds of partially ordered sets called domains. Domain theory is used to specify denotational semantics, especially for functional programming languages. Category theory, as another example, formalizes mathematical structure and its concepts in terms of a collection of objects and of arrows (also called morphisms). Category theory provides powerful modeling idioms and has deep connections to types in programming languages. Concurrency theory studies formalisms for modeling and analyzing concurrent systems. Proof Theory is of major interest in Sub-volume B of Volume B research, and a distinguished result is the Curry–Howard Correspondence, which provides a direct relationship between types in computer programs and formal proofs in certain logics.

The split between Sub-volumes A and B within Volume-B research can perhaps be traced to the standard division of mathematical Logic into several branches: computability theory, model theory, proof Theory, and set Theory. (See the 1989 Handbook of Mathematical Logic, with John Barwise as editor.) While set theory has no clear computer-science counterpart, Sub-volume A of Volume-B research can be traced to computability theory and model theory, while Sub-volume B of Volume-B research can be traced to proof theory. Indeed, a scientific discipline, as it grows and matures, inevitably grows branches, which gradually grow apart from each other. As scientists are forced to go deeper, it becomes gradually impossible for them to keep track of developments in more than a very small number of branches. In fact different branches develop their own specialized languages, impeding communication between branches.

It is often at the interfaces between branches, however, that the most exciting developments occur. Consider Artificial Intelligence, for example. Since the establishment of the field in the late 1950s, logic has played a key role as the fundamental formalism for describing reasoning. Ultimately, however, logical tools were not fully adequate to capture the common-sense reasoning that characterizes human reasoning. In the 21^st Century, probabilistic and statistical approaches have become dominant, for example, in machine learning. Synthesizing the logical and probabilistic approaches is a new frontier, where I expect to see many exciting developments in the next few years.

Finally, while 25 years ago computing-research took place mostly in North America and Western Europe, computing research has since globalized. The Atlantic Ocean is no longer as dominant as it used to be. I look forward to the day when we will write about “The Two Sides of the Pacific/Indian Ocean in Logic and Computation.”