Wednesday, January 18, 2017

Report on the first two days of SOFSEM 2017 (guest post by Ignacio Fábregas)

Ignacio Fábregas has kindly sent me this report on the first two days of SOFSEM 2017, which is being held this week in Limerick, Ireland. I hope you'll enjoy reading it.  Many thanks to Ignacio for agreeing to write this guest post.
SOFSEM has always be an atypical conference with a format closest to a Winter School. This year marks a new beginning for the SOFSEM conference, since it's the first time it's held outside the Czech Republic or the Slovak Republic. As Jan van Leeuwen told us in the Welcome Reception on Monday, the goal of the Steering Committee of SOFSEM is to keep the spirit of SOFSEM alive while moving to a more typical format for a computer science conference. The main ingredients are still there: the keynote talks of renowned experts, tutorial sessions and the Student Research Forum; the only main difference is the country (Ireland) and the schedule (instead of having all the keynote talks the first and last day, now they are distributed across the conference days).

The first day of the Conference the keynote speaker was Kim G. Larsen. He told us about Cyber-Physical Systems (CPS), that is, systems combining computing elements with dedicated hardware and software having to monitor and control a particular physical environment. In order to study them, Larsen and his team propose a model-based approach, powered by the use of the tool Uppaal. An example of CPS is the adaptive cruise control for cars, an application where Europe is trying to match U.S. (where the Google Self-Driving car has already been approved by the legislation in several U.S. states) and where the team of Kim Larsen is making advances.

After the keynote talk we had the first parallel sessions: two sessions of the Foundations of Computer Science (FOCS) track and the first tutorial. I went to the FOCS session about Semantics, Specification and Compositionality, mainly because my talk was there :) But, more importantly, there was a talk of Uli Fahrenberg and another by Linda Bordo. Uli talked about behavioural specification theories for most equivalences in the linear-time–branching-time spectrum. He humbly defined his work as "almost" a rewriting of some old and overlooked results. Going back, reading and, most importantly, understanding, old results is a non-trivial exercise that computer science researchers should do more often. On the other hand, Linda talked about link-calculus, as a model that extends the point-to-point communication discipline of Milner’s CCS with multiparty interactions. She used links to build chains describing the flow of information among the agents participating in that interaction. The difficult part comes when deciding both the number of participants in an interaction and how they synchronize.

The second day of conference we had two keynote talks. Axel Legay talked about Software Product Lines (SPL), that is, the families of similar software products built from a common set of features. For example, like the mobile phones that a company as Samsung or HTC produce. He showed us how he and his team formalizes SPLs by means of what they called Featured Transition Systems and how the designed verification algorithms and tools to check temporal properties over them. The second keynote talk was by Marjan Mernik. He told us about Domain-Specific Languages that assist software developers in programming, and some open problems in the field like the lacking of tool support for different Domain-Specific Languages and the difficulties combining them.

Relative to the conference papers, in the FOCS session in Verification and Automated System Analysis we have talks by Mohammad Reza Mousavi, Nataliya Gribovskaya, Zhaowei Xu and Saket Saurabh. I want to highlight Mohammad's talk about the complexity of deriving invertible sequences from finite-state machines. The problem is the following: checking the existence of input/output sequences (UIOs) that identify states of the finite state machine specification (as it's the case of ioco) is PSPACE-complete; so some UIO generation algorithms utilise what are called invertible sequences; these allow one to construct additional UIOs once a UIO has been found. Mohammad and his coauthors studied some optimization problems and their complexity.

And that's all for now. Tomorrow (18 January 2017) we'll have fewer talks since we have the excursion and conference dinner. Also I'm planning to go for one tutorial session by Andrew Butterfield. I'll tell you more on that.

Thursday, January 12, 2017

Has the Feder-Vardi dichotomy conjecture been proved?

The Feder-Vardi dichotomy conjecture (which, as far as I know, stems from this 1998 article) is a celebrated open problem in the study of the complexity of constraint satisfaction problems (CSPs). It states that, for every finite relational structure, the set of all CSPs that can be represented using only relations chosen from that set is either in P or is NP-complete.

A paper claiming a solution to the Feder-Vardi  conjecture appeared yesterday on the arXiv:

Tómas Feder is the third author. (However, I noticed that the order of the authors in the version of the paper Feder posted on his web page is different from the one used in the arXiv version.)

The authors have also posted two videos on YouTube:

If the technical content of the paper is found to be correct by the community working on CSPs after careful peer review, this is a truly major result.

Wednesday, January 11, 2017

Call for Nominations for Scientific Directorship in Algorithms and Complexity at the Max Planck Institute for Informatics

The Max Planck Institute for Informatics in Saarbrücken is seeking nominations for the position of Scientific Member of the Max Planck Society and Director of the Institute. The founding director, Kurt Mehlhorn, will be retiring in the next three years, and the Institute is looking for a new scientific director for the algorithms and complexity department. (More precisely, Kurt will step down as Director on the day a new director joins. He will stay on as a researcher at the Institute.)

Webpage with the details of the call for nominations: (Self-nominations are possible.)


Friday, December 23, 2016

Mariangiola Dezani-Ciancaglini: 70, but still going strong

Mariangiola Dezani-Ciancaglini, one of the most influential Italian (theoretical) computer scientists, turned 70 yesterday. As witnessed by her DBLP entry, Mariangiola is still very active in research and is a prime example of a scientist who continues to challenge herself, to produce excellent work and to mentor young researchers at an age at which many are retired.

The purpose of this post is to celebrate Mariangiola's 70 birthday, hoping that some of the readers of this blog who are not familiar with her work will be tempted to read it and to spread it amongst their students.

Mariangiola Dezani has been one of the leading researchers in the foundations of programming languages and, in particular, of their type systems for about 40 years. She has offered seminal contributions to that field, introducing new type systems that deeply influenced theoretical developments and its practical applications.

In addition to her outstanding research activities, she has been a mentor and role model for young researchers, many of whom now have leading positions at high-class universities. Moreover, she has tirelessly supported female students and researchers in computer science at all stages of their career. She has turned the Department of Computer Science at the University of Turin, Italy, into a hotbed of research on the theory of programming languages. The group led by Simona Ronchi Della Rocca and her is one of the largest research teams in that field in the world, and is one of those with largest percentage of female researchers and students.

Mariangiola's research activity over the years has followed a path in which theoretical developments have been inspired by the evolution of programming languages: from lambda-calculus models in the 1980s, providing foundations for functional programming languages, to object orientation in the 1990s, to dynamic and distributed contexts with behavioural types for web services and session types since the year 2000.

Mariangiola's main scientific achievement in the first phase of her research career was the introduction of intersection type assignment systems, which were largely used as finitary descriptions of models of the lambda-calculus. Intersection types are one example of a theoretical concept developed by Mariangiola Dezani that has later had profound influence on the practice of programming languages. Indeed, their use in the typing discipline for a language has allowed compilers to generate more efficient code for different instantiations. In object-oriented languages, intersection types are employed, amongst other things, in expressing mixins (constructs that permit code reuse avoiding the ambiguities of multiple inheritance). They have also been advocated and are used for manipulating XML and semi-structured data in languages such as CDuce.

Since the year 2000, Mariangiola's research has been mainly devoted to the study of self-adapting types for ensuring safety and liveness of communication protocols also in presence of unexpected events. This work has offered seminal contributions to the study of session types and has led to practical applications whose impact will be felt for years to come. Mariangiola first proposed a formalisation of Java with session types, which was later applied to the design and implementation of SJ (Session Java). These contributions initiated a flurry of research activity aiming at applying session types to many real-world programming languages. She also first studied a theory of progress in the session types for the pi-calculus, whose core theory was later extended to multi-party session types. This formalism became the core of the current version of an open-source protocol description language, Scribble, which is developed at Red Hat and Imperial. This language is used in the multi-million-USD Ocean Observatory Initiative project, whose purpose is to build an infrastructure of sensors and other computing devices located on the ocean floor so that oceanographers to get data about the health of the marine ecosystem. This is an example of the effectiveness and practical impact of the deep and elegant theoretical work carried out by Mariangiola Dezani.

A belated happy 70th birthday, Mariangiola!

Monday, December 05, 2016

Great hiring opportunities for female researchers at the University of Groningen

Jorge A. Pérez asked me to post this very interesting opportunity for tenure-track positions at the University of Groningen, targeted to talented female researchers (see Feel free to contact Jorge if you work in areas related to "Fundamental CS" (using the terminology in the call) and are interested in applying.

Rosalind Franklin Fellowships at the University of Groningen

The University of Groningen (The Netherlands) initiated the prestigious Rosalind Franklin Fellowship programme to promote the advancement of talented international researchers at the highest levels of the institution. The ambitious programme has been running since 2007 and has financed over 90 Fellows.

The Rosalind Franklin Fellowship programme is aimed at women in industry, academia or research institutes who have a PhD and would like a career as full professor in a European top research university. The Fellowship is only awarded to outstanding researchers. New Fellows are given:
  • A tenure track position to work towards full professorship within a period of ten years;
  • Budget for a PhD student to enable them to make a flying start.
Successful candidates will be expected to establish an independent, largely externally funded research programme in collaboration with colleagues at
our University and elsewhere.

The University of Groningen has 13 tenure track positions available in this programme, currently co-funded by the European Union.
Within these, the Faculty of Mathematics and Natural Sciences (FMNS) has five Rosalind Franklin Fellowships to offer, including positions on
  • Fundamental Computer Science (Data Management, Theory of Computing, Algorithms, Networks, Security)
  • Artificial Intelligence (logic, neuromorphic computing, cognitive modelling or robotics)
  • Fundamental Mathematics (Algebra, Geometry, Analysis), Mathematical Data Analysis, Complex Systems
Ambitious female academics are invited to apply for these positions before February 1, 2017.

More information about the positions (including eligibility conditions and conditions of employment) is available on:

See also:
- The applicants guide:

- The Johann Bernoulli Institute for Mathematics and Computer Science:

Martino Lupini receives the 2015 Sacks Prize of the Association for Symbolic Logic

The 2015 Sacks Prize of the Association for Symbolic Logic for the best doctoral dissertation in Logic will be shared by Omer Ben-Neria, University of California, Los Angeles, and Martino Lupini, California Institute of Technology. The prize citations can be found here and are also appended to this post for ease of reference.  Congratulations to the prize recipients!

Omer Ben-Neria received his Ph.D. in 2015 from Tel Aviv University under the supervision of Moti Gitik.

Martino Lupini received his Ph.D. in 2015 from York University, Toronto under the supervision of Ilijas Farah. He received his bachelor degree at the University of Parma (under the supervision of Celestina Cotti Ferrero) and a master degree from the University of Pisa advised by Mauro Di Nasso with a thesis entitled Recurrence and Szemerédi’s Theorem.

Martino Lupini is the second Italian young researcher to receive this accolade; the first was Matteo Viale in 2006. The successes of young Italian logicians witness the quality of the research in logic in Italy. This is yet another vindication of the analysis of the European Commission on the quality of research in Italian universities, compared with the resources available to Italian researchers: "Strong public science base despite an overall underinvestment in research and innovation." The executive report on Italy also states "R&D investment has slightly increased in recent years but the gap with the EU average is still quite significant." I hope that Italy will devote more of its budget to supporting its universities and research in the future. A starved system cannot continue producing young researchers like Martino Lupini for much longer.

Prize citations

Ben-Neria received his Ph.D. in 2015 from Tel Aviv University under the supervision of Moti Gitik. In his thesis, The Possible Structure of the Mitchell Order, he proved the remarkable result that, under suitable large cardinal assumptions on the cardinal $\kappa$, every well-founded partial order of cardinality $\kappa$ can be realized as the Mitchell order of $\kappa$ in some forcing extension. The Prizes and Awards Committee noted that the proof is a tour de force combination of sophisticated forcing techniques with the methods of inner model theory.

Lupini received his Ph.D. in 2015 from York University, Toronto under the supervision of Ilijas Farah. His thesis, Operator Algebras and Abstract Classification, includes a beautiful result establishing a fundamental dichotomy in the classification problem for the automorphisms of a separable unital $C^*\/$-algebra up to unitary equivalence, as well as a proof that the Gurarij operator space is unique, homogeneous, and universal among separable 1-exact operator spaces. The Prizes and Awards Committee noted that his thesis exhibits a high level of originality, as well as technical sophistication, in a broad spectrum of areas of logic and operator algebras.

Alonzo Church Award 2017: Call for Nominations

Gordon Plotkin asked me to post the call for nominations for the 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation. The first edition of the award was given to Rajeev Alur and David Dill for their invention of timed automata, see: I strongly encourage members of the community to nominate their favourite paper(s) for this accolade. See the call for the rules regarding eligibility and on how to submit your nomination. 

The 2017 Alonzo Church Award for Outstanding Contributions to Logic and Computation

Call for Nominations


An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see:

The 2016 Alonzo Church Award was given to Rajeev Alur and David Dill for their invention of timed automata, see:

Eligibility and Nominations

The contribution must have appeared in a paper or papers published within the past 25 years. Thus, for the 2017 award, the cut-off date is January 1, 1992. When a paper has appeared in a conference and then in a journal, the date of the journal publication will determine the cut-off date. In addition, the contribution must not yet have received recognition via a major award, such as the Turing Award, the Kanellakis Award, or the Gödel Prize. (The nominee(s) may have received such awards for other contributions.) While the contribution can consist of conference or journal papers, journal papers will be given a preference.

Nominations for the 2017 award are now being solicited. The nominating letter must summarise the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness.

Nominations are due by March 1, 2017, and should be submitted to

Presentation of the Award

The 2017 award will be presented at the CSL conference, the annual meeting of the European Association for Computer Science Logic. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared.

Award Committee

The 2017 Alonzo Church Award Committee consists of the following four members: Natarajan Shankar, Catuscia Palamidessi, Gordon Plotkin (chair), and Moshe Vardi.

Monday, November 21, 2016

Academic evaluation and hiring in Italy: The curious incident of Giovanni Sambin in the ASN 2016

Disclaimer: This post might contain imprecisions about the ASN, since I have never worked at an Italian university myself and I have never applied for the Italian ASN. I welcome corrections from whoever reads this post and has experience with this Italian evaluation exercise. Let me state at the outset that what I write pertains to fields such as computer science and mathematics. I do not know what is done in the humanities. 

An Italian law dated 30 December 2010 specifies a procedure for academic hirings in Italy at the level of associate and full professor. According to that law, recruiting for those positions should be "based on scientific qualification criteria. A national commission evaluates and assesses the candidates scientific qualification." See this outdated web site, which should be compared with the one in Italian.  Only candidates that have obtained the so-called Abilitazione Scientifica Nazionale (ASN, National Scientific Qualification) can then apply for a professor position at an Italian university, if and when such positions are advertised.

One can wonder why Italy uses this two-step system for academic hirings, whose need is not felt in any of the countries where I have worked so far. I guess that the first step is meant to filter out potential candidates who do not meet minimum requirements for being a professor at any of the 63 public universities in Italy. 

According to the regulations a "national commission evaluates and assesses the candidates scientific qualification." In fact, there is one national commission for each of the many scientific areas considered in Italy. Many of these commissions have to examine hundreds of applications, and their members play the role of gatekeepers and paladins of quality in the Italian university system. I can only imagine how much work is needed to do a thoughtful job in one of those committees and how easy it is to make enemies regardless of how considerate one is in justifying one's opinions. The evaluation is partly based on bibliometric criteria, which are known beforehand, should simplify the work of the commissions and should give a look of objectivity to their decisions. However, as far as I know, the commissions can also base their decisions on a qualitative analysis of the applicants.

Given the crucial role played by the members of the evaluation committees, one would expect that their members are chosen by taking the candidates' scientific profile and experience carefully into account. As it turns out, however, the qualifications of candidates for the committee are evaluated using only the following three bibliometric criteria:
  1. Number of publications in the period 2006-2016 (threshold 9);
  2. Total number of citations  in the period 2001-2015 (threshold 80);
  3. H-index in the last 15 years (threshold 5). 
In order to be eligible, one has to meet the thresholds in at least two of the above criteria. This might even seem reasonable. Note, however, that only publications indexed in Web of Science or Scopus count. In particular, journal papers published in outlets that are not indexed by Web of Science/Scopus are not taken into consideration (regardless of their content and impact) and conference papers don't count at all. Books and monographs don't count either, regardless of how influential they might be. Web of Science/Scopus are also used for calculating citations and the h-index. Again, this provides a smaller coverage than the one offered by Google Scholar, say.

By way of example, recently Giovanni Sambin, one of the most famous, currently active Italian logicians and an expert academic  one would trust to lead a national evaluation committee for Mathematical Logic, was considered to be ineligible as an evaluator because he met only one of the above-mentioned criteria. His Google Scholar profile is here.

This kind of decisions makes me wonder whether there is an overemphasis on bibliometric evaluations in Italian academia. If experience over a long and distinguished academic career plays second fiddle to fairly arbitrary thresholds calculated using only Web of Science and Scopus, I wonder how reliable the decisions of the evaluation committees will be considered by Italian academics. Most importantly, having so many people spend a lot of time seeking the holy grail of the national qualification and small committees devote endless hours examining their qualifications looks like a huge waste of energy and resources. I cannot help but think that that energy and time would be best used for research, teaching and all the other tasks that make up our work.

Tuesday, November 15, 2016

Workshops at LICS 2017

The following six workshops will be co-located with LICS 2017 and will take place on Monday, 19 June 2017, on the premises of Reykjavik University:
  • WiL: Women in Logic. Proposers: Valeria de Paiva, Amy Felty, Anna Ingolfsdottir, Ursula Martin
  • LCC: Logic and Computational Complexity. Proposers: Norman Danner, Anuj Dawar, Isabel Oitavem, Heribert Vollmer
  • LMW: Logic Mentoring Workshop. Proposers: Anupam Das, Valeria Vignudelli, Fabio Zanasi
  • LA: Learning and Automata. Proposers: Borja Balle, Leonor Becerra-Bonache, Remi Eyraud
  • LOLA: Syntax and Semantics of Low-Level Languages. Proposer: Matija Pretnar, Noam Zeilberger
  • Metafinite model theory and definability and complexity of numeric graph parameters. Proposers: Andrew Goodall, Janos A. Makowsky, Elena V. Ravve.
More details on this workshops will be available from the conference web page in due course. I hope that you'll consider attending them and submitting excellent papers to the conference.