π-calculus, Session Types research at Imperial College

The Kohei Honda Prize for Distributed Systems Queen Mary, University of London

Posted with permission from QMUL on 17th Dec 2013. Original article written by Edmund Robinson. Featured in Bulletin of EATCS: [1]

This prize was instituted in 2013 and is awarded annually to one undergraduate student and one postgraduate student in recognition of their achievement in applying the highest quality scientific and engineering principles in the broad area of Distributed Systems. This is the area in which Dr Honda concentrated most of his teaching, and it is also the area in which he conducted his research. Its primary funding comes from a donation from his family, who wished to commemorate Dr Honda in this way. Additional funding has come from Dr Honda’s own ETAPS Award. This prize is sponsored by Springer Verlag, and awarded annually by the ETAPS committee in recognition of an individual’s research contribution. Dr Honda received the first such award posthumously, and the awarding panel expressed a wish that the funding be used to supplement this prize fund. The laudation for this award, written by Dr Honda’s colleague, Prof Vladimiro Sassone is included later.

About Dr Honda

Dr Kohei Honda
Dr Kohei Honda

Kohei Honda was born and lived the first part of his life in Japan. Like many scientists he was fascinated by the idea of finding basic explanatory theories, like the physicists looking for grand unified theories of the universe. Kohei, though, was passionately interested in finding the right basic explanatory theory for the process of computation. Most academics agree that the basic theory of the foundations of computation, set out by Church and Turing in the 1930’s, is fine for simple computations on a single computer, but does not really account for processes of computation spread across a number of locations, as our modern web-based, cloud-based computation now is. (Ananalogy is the physicists recognition that their theories account for electrical and atomic forces, but not gravity). Kohei believed he had found this in the theory of process calculi being developed by a number of researchers, and, in particular, in Robin Milner’s pi-calculus.

Very early on in his career, Kohei developed a form of this calculus adapted to asynchronous communications (communications where delivering a message can take time, and where the system may never be in a perfect state where the sender has just successfully sent a message and the receiver has just successfully received it).

Kohei came to the UK to develop his work, spending time in Manchester and Edinburgh, before eventually settling in London at Queen Mary. Working with his partner, Nobuko Yoshida, he produced a stream of work which was at first theoretical. Powerful results showed that the pi-calculus was expressive enough to account for many forms of computation through the use of restrictions on the communications allowed. The key point here is not that the calculus is powerful enough to mimic the various systems (that is easy), but that the restrictions can be made strong enough to rule out things that are not computable in the system being studied.

This work gave Kohei great insight into the way the structure of communication between different processors could be used to restrict the calculations they performed. He went on to apply this in work on web services choreography with the World Wide Web Consortium (finding means of specifying how different web services could be gluedtogether in safe ways). This was followed by the development of a specification language: Scribble. His goal was to enable system developers to ensure that the components of their systems (which might be distributed all over the world and even beyond) were behaving in a safe and controlled way. That goal is one which goes to the heart of our modern use of computers as they enter into all aspects of our lives, and yet are controlled remotely over the internet.

At the time of Kohei’s tragic death, his ideas were really taking off, and they are now being developed through a major project based at Imperial, where his wife continues to work, and Edinburgh, where he himself spent a period in his youth. This, however, was only one part of Kohei’s work at Queen Mary. He was also a dedicated teacher. He was fully aware of the need to assist students to gain practical skills, and at the same time had amazing skill in boiling down an issue to its essentials. He spent a good deal of time working with, helping and guiding individual students. He regarded training the next generation as one of the key duties and also benefits of being an academic.

His post as Reader is an unusual one. It is our recognition that Kohei had a brilliant mind. But he was interested in science and teaching, not in administration or running a department as full Professors have to. Kohei’s readership harks back to earlier times where it was the post for brilliant academics who were not administrators. It is the post that Alan Turing held at Manchester, and the comparison is not inappropriate.

Winners 2013

Ms Anna Pawlicka
Ms Anna Pawlicka
2013 winner (Undergraduate) source: QMUL
Mr Valdmir Negacevschi
Mr. Valdmir Negacevshi
2013 winner (Postgraduate) source: QMUL

Winners 2014

Filippo Charuttini
Joana Vasileva

Winners 2015

Reza Abedian
Tian Yang
#### ETAPS Award
LAUDATIO for KOHEI HONDA A rare cluster of qualities: curiosity, passion and perception; all at the perfect pitch of passion and expression.

Kohei Honda (1959–2012) died of cerebral haemorrhage on December 4th, 2012. He received an MSc (1991) and a PhD (1994) in Computer Science from Keio University, in Yokohama, Japan. Kohei started to show his talent already as a student: strikingly, even before completing his MSc, he had published a milestone paper which revolutionised the field of processes calculi by showing us how to formalise asynchronous communications.

Kohei moved to Europe in 1995 and held positions at the Universities of Manchester, Edinburgh, and Queen Mary University of London, where he was made a reader in October 2002. He has been official external advisor of WS-CDL, ISO TC68 WG4 UNIFI (UNIversal Financial Industry message scheme) and AMQP (Advanced Message Queueing Protocols). He was the initiator of JBoss Scribble, and worked with several industrial partners, including Cognizant, Red Hat, VMware, Bank of Japan, Hitachi and UBS, as well as in the multidisciplinary Ocean Observatories Initiative.

The team of the Ocean Observatories Initiative CyberInfrastracture remembers him as possessing a rare cluster of qualities: “His aesthetics, precision and enthusiasm for our mutual pursuit of formal session types […] were, as penned by Henry James, lessons in seeing the nuances of both beauty and craft, through a rare cluster of qualities – curiosity, patience and perception; all at the perfect pitch of passion and expression."

Indeed Kohei was a dedicated, passionate, enthusiastic scientist and –more than that!– his enthusiasm was contagious. He was a theoretician who really succeeded in building bridges with practitioners. The collaboration between Kohei and his team, W3C, Steve Ross-Talbot and Robin Milner transformed into Pi4 Technologies and then into Savara and gave birth to Scribble, his own language for the description of application-level protocols among communicating systems. Among Kohei’s milestone research, I have already mentioned his 1991 epoch-making paper at ECOOP (with Mario Tokoro) on the treatment of asynchrony in message passing calculi, which has influenced all process calculi research since. Furthermore, Kohei established the first fully abstract model for call-by-value programming languages and demonstrated deep connections between game semantics and process calculi. At ETAPS 1998 he introduced (with Vasco Vasconcelos and Makoto Kubo) a new concept in type theories for communicating processes: it came to be known as ‘session types’, and has since spawn an entire research area, with practical and multi-disciplinary applications that Kohei was just starting to explore –as always in partnership, in life as in research, with his wife Nobuko Yoshida.

Kohei leaves behind him enormous impact, and a lasting legacy. He is irreplaceable, and I for one am proud to have been his colleague and glad that ETAPS took the opportunity to award to him, albeit posthumously, this first edition of the ETAPS Award.

Featured in Bulletin of the EATCS: [2].