I am pleased to post Davide Sangiorgi's interview with CONCUR 2022 Test-of-Time Award recipient James Leifer, who will receive the award for the paper

"Deriving Bisimulation Congruences for Reactive Systems" co-authored with the late Robin Milner.

Thanks to James for painting a rich picture of the scientific and social context within which the work on that paper was done and to Davide for conducting the interview. I trust that readers of this blog will enjoy reading it as much as I did.

**Davide:**How did the work presented in your CONCUR ToT paper come about?

**James:**I was introduced to Robin Milner by my undergraduate advisor Bernard Sufrin around 1994. Thanks to that meeting, I started with Robin at Cambridge in 1995 as a fresh Ph.D. student. Robin had recently moved from Edinburgh and had a wonderful research group, including, at various times, Peter Sewell, Adriana Compagnoni, Benjamin Pierce, and Philippa Gardner. There were also many colleagues working or visiting Cambridge interested in process calculi: Davide Sangiorgi, Andy Gordon, Luca Cardelli, Martín Abadi,... It was an exciting atmosphere! I was particularly close to Peter Sewell, with whom I discussed the ideas here extensively and who was generous with his guidance.

*P*and

*Q*, and all process contexts

*C[-]*, if

*P ~ Q*, then

*C[P] ~ C[Q]*. This is a key quality for a bisimulation to possess, since it allows modular reasoning about pieces of a process, something that's so much harder in a concurrent world than in a sequential one.

*P*undergoing the input labelled transition

*xy*could be thought of as the environment outputting payload

*y*on channel

*x*to enable a tau transition with

*P.*

*P ---C[-]---> P'*to mean

*C[P] ------> P'*provided that

*C[-]*was somehow "minimal", i.e. contained nothing superfluous beyond what was necessary to trigger the reaction. We wanted to get a rigorous definition of that intuitive idea. There was a long and difficult period (about 12 months) wandering through the weeds trying to define minimal contexts for Action Calculi graphs (in terms of minimal nodes and minimal arcs), but it was hugely complex, frustrating, and ugly and we seemed no closer to the original goal of achieving congruential bisimulation with these labelled transitions systems.

*R ------> R'*, we can define labelled transitions

*P ---C[-]---> P'*as follows: there exists a context

*D*such that

*C[P] = D[R]*and

*P' = D[R']*. The first equality is a commuting diagram and Robin and I thought that we could formalise minimality by something like a categorical pushout! But that wasn't quite right as

*C*and

*D*are not

*the minimum*pair (compared to all other candidates), but

*a minimal*pair: there may be many incomparable minimal pairs all of which are witnesses of legitimate labelled transitions. There was again a long period of frustration eventually resolved when I reinvented "relative pushouts" (in place of pushouts). They are a simple notion in slice categories but I didn't know that until later...

*P ~ Q*implies

*E[P] ~ E[Q]*. For weeks, I was considering the labelled transitions of

*E[P] ---F[-]--->*and all the ways that could arise. The most interesting case is when a part of

*P,*a part of

*E*, and

*F*all "conspire" together to generate a reaction. From that I was able to derive a labelled transition of

*P*by manipulating relative pushouts, which by hypothesis yielded a labelled transition of

*Q*, and then, via a sort of "pushout pasting", a labelled transition

*E[Q] ---F[-]--->*. It was a wonderful moment of elation when I pasted all the diagrams together on Robin's board and we realised that we had the congruence property for our synthesised labels!

**Davide:**What influence did this work have in the rest of your career? How much of your subsequent work built on it?

**James:**It was thanks to this work that I visited INRIA Rocquencourt to discuss process calculi with Jean-Jacques Lévy and Georges Gonthier. They kindly invited me to spend a year as postdoc in 2001 after I finished my thesis with Robin, and I ended up staying in INRIA ever since. I didn't work on bisimulation again as a research topic, but stayed interested in concurrency and distribution for a long time, working with Peter Sewell et al on distributed language design with module migration and rebinding, and with Cédric Fournet et al on compiler design for automatically synthesising cryptographic protocols for high level sessions specifications.

**Davide:**Could you tell us about your interactions with Robin Milner? What was it like to work with him? What lessons did you learn from him?

**James:**I was tremendously inspired by Robin.

**Davide:**What research topics are you most interested in right now? How do you see your work develop in the future?

**James:**I've been interested in a totally different area, namely healthcare, for many years. I'm fascinated by how patients, and information about them, flows through the complex human and machine interactions in hospital. When looking at how these flows work, and how they don't, it's possible to see where errors arise, where blockages happen, where there are informational and visual deficits that make the job of doctors and nurses difficult. I like to think visually in terms of graphs (incrementally adding detail) and physically moving through the space where the action happens --- all inspired by Robin!