An interview with Hans Hüttel, CONCUR Test-of-Time Award recipient

This post is devoted to the fourth, and last, interview with the colleagues who were selected for the first edition of the CONCUR Test-of-Time Award. (See here for the interview with Davide Sangiorgi,  here for the interview with Nancy Lynch and Roberto Segala, and here for the interview with Rob van Glabbeek.) In keeping with my previous interviews, I asked  Hans  Hüttel (Aalborg University, Denmak) a few questions via email and you can find his answers below. 

Hans receives the award for his paper "Bisimulation Equivalence is Decidable for all Context-Free Processes", which he wrote  with Søren Christensen and Colin Stirling. Søren moved to industry after finishing his PhD. Colin is now retired. 

Luca: You receive one of the two CONCUR ToT Awards for the period 1990-1993 for the paper  "Bisimulation Equivalence is Decidable for all Context-Free Processes" you published with Søren Christensen and Colin Stirling at CONCUR 1992. Could you tell us briefly what the context for that work was and how it came about?

Hans: I was working on my PhD which was on the topic of decidability of behavioural equivalences for process calculi that allow processes to have infinite state spaces. Baeten, Bergstra and Klop had proved that strong bisimilarity is in fact decidable for the BPA calculus even though the class of trace languages for BPA is exactly the class of context-free languages. The result only held for normed BPA processes, that is, processes that could always terminate. Colin was my supervisor in Edinburgh, and he suggested that I try to find a simpler proof of that result (much can be said about the original proof, but simple it was not!). This turned out to be really interesting; I met Didier Caucal from IRISA who had found a nice, much shorter proof that relied on finite characterizations and I was able to use his notion of self-bisimilarity to prove that a tableau system for bisimilarity was sound and complete wrt. bisimilary. Jan Friso Groote, who was a PhD student at the CWI at the time, and myself proved that all other known equivalences are undecidable for normed BPA (and therefore a fortiori also for full, unnormed BPA). But one problem that Colin and I were never able to solve was if the decidability result also held for the full BPA calculus.

Søren arrived in Edinburgh in 1990 and we shared a flat there, in St Leonards Bank just across from Holyrood Park. We hung out with the same people in the LFCS, many of whom were clever Italians such as Davide Sangiorgi and clever quasi-Italians such as Marcelo Fiore. It is no surprise that Søren and I often discussed our work or that he, given that Colin was also his supervisor, moved on to study decidability problems as well, the only difference being that Søren was mostly interested in the BPP calculus that has parallel composition instead of sequential composition.

When I left Edinburgh at the end of August of 1991, Colin and I had managed to make some progress on the decidability problem for unnormed BPA. We realised that a finite characterization of the maximal bisimulation á la Caucal was the way ahead but the actual characterization escaped us. When I returned for my viva in December, Søren had found an important lemma on finite characterizations and everything fell into place. The decidability result relied on proving that bisimilarity is semi-decidable using the finite characterization; non-bisimilarity was already known to be semi-decidable.

Luca: Both Søren Christensen and you wrote the award-winning paper as PhD students in Edinburgh. Could you tell us about the research environment in Edinburgh at that time, and the influence it had on you then and in the rest of your career?

Hans: The LFCS in Edinburgh was a great place to be at the time. Robin Milner was still around and busy working on the pi-calculus together with Davide Sangiorgi, who was his student at the time. Watching them at the blackboard was interesting, even though the rest of us often could not follow their discussions! Gordon Plotkin was there (and still is, fortunately). Rod Burstall was still active, and so was Mike Fourman. Plus many, many others. There was always someone to talk to, and it was perfectly legitimate to have an interest in basic research. Unlike the other professors, Colin had no background in maths – he was originally a philosopher! – and maybe that was why he was trying to avoid heavy mathematical lingo, trying to be simple and precise in his writing at the same time. I learned a lot from him, also in that respect.

After Søren returned to Denmark, he left academia and got a job in the private sector. He still lives near Aarhus. Sadly we lost touch with each other, in all likelihood because our lives turned out so different. We got back in touch recently, when we were told about the reward and we look forward to finally meeting each other again. Colin retired recently, and I really hope to see him again, when I am able to travel to Scotland again some day.

Luca: How much of your later work has built on your award-winning paper? What follow-up results of yours are you most proud of and why?

Hans: I worked on decidability issues for another few years after that but there was no-one to talk to in Aalborg, or rather, there was no-one there that shared my interest in the area at the time. What is more, the open problems that remained were major challenges. Some were only solved much later (such as the decidability of bisimilarity for pushdown automata, a result due to Sénizergues, the proof later greatly simplified by Colin) or remain open (such as the decidability of weak bisimilarity for BPA). Eventually I drifted down the slippery slope and became interested in other, related topics, and focused somewhat more directly on program properties. The follow-up result that most directly relates to my paper with Søren and Colin is the result from 1994 that bisimilarity is also the only equivalence that is decidable for BPP. This is a result that I am also quite proud of. It grew out of discussions with Javier Esparza and Yoram Hirshfeld, when I was back in Edinburgh for a while in 1993. Ironically, there was a subtle flaw in the proof that Naoki Kobayashi discovered many years later. Naoki and one of his student found out how to repair the proof, and the three of us co-authored the journal version that came out many years later. The reason why Naoki became interested in BPP was that he was trying to use the calculus as a behavioural type system for a pi-calculus. As it happened, this was also the route that I had taken.

Those of my later results that I am most proud of have to do with this area: My work on type systems for psi-calculus (CONCUR 2011 and later) and a session type system for bounded name use in the pi-calculus (Acta Informatica 2019). The latter paper also has a CONCUR connection; it grew out of attending a talk by Roland Meyer at CONCUR 2013 and wondering why they were not trying to characterize notions of name-boundedness in the pi-calculus by means of a type system. It turned out that Meyer et al. were not familiar with type systems at all. It took me an awful long time to work out a type-based characterization (using session types), as you can probably tell.

As you can tell, I have not worked on bisimulation for quite some time. Not that there is anything wrong with bisimulation, of course, but if one wants results that are applicable for automated reasoning about program behaviour, decidability is important. One can then either choose to go for a less expressive model of computation (which is what researchers in the model checking community do) or keep the model of computation and go for sound, but incomplete characterizations of program properties (which is what researchers interested in type systems and related static analysis methods do). I ended up in the latter camp.

Luca: To your mind, what are the most interesting or unexpected uses in the literature of the notions and techniques you developed in "Bisimulation Equivalence is Decidable for all Context-Free Processes"?

Hans: BPA, BPP and similar process calculi can be used as the basis of behavioural type systems, and I am thrilled that my old research interests and my current research interests are so directly related.

In 2018 I discovered that Vasco Vasconcelos and Peter Thiemann had devised a session type system for a functional programming language in which session types were not regular expressions (which is essentially what they are in the original work by Honda, Kubo and Vasconcelos) but BPA processes. Vasco and Peter knew that type equivalence should be decidable but they were not so familiar with our results from the early 1990s. At POPL 2019 I attended a talk by Andreia Mordido, one of Vasco’s collaborators, and she mentioned our paper from CONCUR 1992! Later that day, I ended up talking to Andreia and Vasco about my work on BPA from all those years ago.

Luca: The last forty years have seen a huge amount of work on process algebra and process calculi. However, the emphasis on that field of research within concurrency theory seems to have diminished over the last few years, even in Europe. What advice would you give to a young researcher interested in working on process calculi today?

Hans: That they should still work on process calculi! There remains a lot of interesting work to be done. One reason why research topics drift in and out of focus is simply that researchers lose interest; it is hardly ever the case that a topic runs out of interesting research questions. Another reason is rather grim: Basic research is nowhere near as well-respected as it used to be. If you look at the funding schemes that we have today, only the very successful few can get funding for basic research; I am not among them and it does get frustrating quite often. Most topics these days deal with applied research. There is nothing wrong with applied research per se; some of what I do is on that side of things, but there has to be more to research than that.

Luca: What are the research topics that currently excite you the most?

Hans: I have slowly become more and more interested in programming language theory, and some of my current collaborators have taken a similar route, beginning in concurrency theory, drifting into the world of behavioural type systems and finally wanting to apply all of their skills to actual programming languages. Right now Mario Bravetti, Adrian Francalanza, António Ravara and myself are involved in working on a behavioural type system related to the Mungo tool for a subset of Java. I am fortunately enough to have had three exceptionally clever and productive MSc students involved as well, and this has been extremely helpful. Mungo is in many ways the work of Simon Gay and Ornela Dardha at Glasgow University, and they, too, began their careers working on process calculi.

Luca: You have a keen interest in teaching at university level. Is there anything you think we should do better in conveying the beauty and usefulness of theoretical computer science in general, and concurrency theory in particular, to our students today? Do you have any thoughts you'd like to share with us on how to combine digital resources and in-person meetings in the teaching of subjects in the theory of computing?

Hans: Personally I think there is a tendency to present any academic topic – and in particular topics in the mathematical sciences, broadly speaking – in such a way that the definitions and theorems appear as if they fell from the heavens, fully formed. As any researcher will know, that is certainly not how they came about. In this way, we focus a lot on what Imre Lakatos and Karl Popper called the context of justification. A well-honed presentation of a theory may appear to be beautiful, but in my opinion the actual beauty is the one that one experiences when one has finally understood the theory and understands why the definitions and theorem turned out the way they did – that is, one must understand the context of discovery. I think problem-based learning (which is something that we talk about a lot at Aalborg University and at Roskilde University) is the key here, because it puts the focus on student-centered active learning.

I have lectured a lot over the years but since 2013 I have drifted away from traditional lectures towards flipped teaching in which I use pre-recorded podcasts (of my own making) that students can watch whenever they want; I then use the plenary sessions for activities that focus on active learning. I by far prefer having a dialogue with students that focuses on the problems that they encounter to the monologue style of a lecture. All my teaching activities are now flipped and I am happy to say that some of my colleagues are now thinking along similar lines. It is always good to have someone to talk to.