Davide Sangiorgi's Interview with James Leifer, CONCUR 2022 ToT Award Recipient

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.

There was a trend in the community at the time of building complex process calculi (for encryption, Ambients, etc.) where the free syntax would be quotiented by a structural congruence to "stir the soup" and allow different parts of a tree to float together; reaction rules (unlabelled transitions) then would permit those agglomerated bits to react, to transform into something new.

Robin wanted to come up with a generalised framework, which he called Action Calculi, for modelling this style of process calculi.  His framework would describe graph-like "soups" of atoms linked together by arcs representing binding and sharing; moreover the atoms could contain subgraphs inside of them for freezing activity (as in prefixing in the pi-calculus), with the possibility of boundary crossing arcs (similarly to how nu-bound names in pi-calculus can be used in deeply nested subterms).  

Robin had an amazing talent for drawing beautiful graphs! He would "move" the nodes around on the chalkboard and reveal how a subgraph was in fact a reactum (the LHS of an unlabelled transition).  In the initial phases of my Ph.D. I just tried to understand these graphs: they were so natural to draw on the blackboard! And yet, they were also so uncomfortable to use when written out in linear tree- and list-like syntax, with so many distinct concrete representations for the same graph.

Putting aside the beauty of these graphs, what was the benefit of this framework? If one could manage to embed a process calculus in Action Calculi, using the graph structure and fancy binding and nesting to represent the quotiented syntax, what then? We dreamt about a proposition along the following lines: if you represent your syntax (quotiented by your structural congruence) in Action Calculi graphs, and you represent your reaction rules as Action Calculi graph rewrites, then we will give you a congruential bisimulation for free!

Compared to CCS for example, many of the rich new process calculi lacked labelled transitions systems. In CCS, there was a clean, simple notion of labelled transitions and, moreover, bisimulation over those labelled transitions yielded a congruence: for all processes 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.

Returning to Action Calculi, we set out to make good on the dream that everyone gets a congruential bisimulation for free! Our idea was to find a general method to derive labelled transitions systems from the unlabelled transitions and then to prove that bisimulation built from those labelled transitions would be a congruence.

The idea was often discussed at that time that there was a duality whereby a process undergoing a labelled transition could be thought of as the environment providing a complementary context inducing the process to react. In the early labelled transition system in pi-calculus for example, I recall hearing that 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.

So I tried to formalise this notion that labelled transitions are environmental contexts enabling reaction, i.e. defining 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.

Eventually I stepped back from Action Calculi and started to work on a more theoretical definition of "minimal context" and we took inspiration from category theory.  Robin had always viewed Action Calculi graphs as categorical arrows between objects (where the objects represented interfaces for plugging together arcs). At the time, there was much discussion of category theory in the air (for game theory); I certainly didn't understand most of it but found it interesting and inspiring.

If we imagine that processes and process-contexts are just categorical arrows (where the objects are arities) then context composition is arrow composition. Now, assuming we have a reaction rule 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...

Having found a reasonable definition of "minimal", I worked excitedly on bisimulation, trying to get a proof of congruence: 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!

We looked back again at Action Calculi, using the notion of relative pushouts to guide us (instead of the arbitrary approach we had considered before) and we further looked at other kinds of process calculi syntax to see how relative pushouts could work there...  Returning to the original motivation to make Action Calculi a universal framework with congruential bisimulation for free, I'm not convinced of its utility. But it was the challenge that led us to the journey of the relative pushout work, which I think is beautiful.

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.

He would stand at his huge blackboard, his large hands covered in chalk, his bicycle clips glinting on his trousers, and he would stalk up and down the blackboard --- thinking and moving.  There was something theatrical and artistic about it: his thinking was done in physical movement and his drawings were dynamic as the representations of his ideas evolved across the board.

I loved his drawings. They would start simple, a circle for a node, a box for a subgraph, etc. and then develop more and more detail corresponding to his intuition. (It reminded me of descriptions I had read of Richard Feynman drawing quantum interactions.)

Sometimes I recall being frustrated because I couldn't read into his formulas everything that he wanted to convey (and we would then switch back to drawings) or I would be worried that there was an inconsistency creeping in or I just couldn't keep up, so the board sessions could be a roller coaster ride at times!

Robin worked tremendously hard and consistently. He would write out and rewrite out his ideas, regularly circulating hand written documents. He would refine over and over his diagrams. Behind his achievements there was an impressive consistency of effort.

He had a lot of confidence to carry on when the sledding was hard. He had such a strong intuition of what ought to be possible, that he was able to sustain years of effort to get there.

He was generous with praise, with credit, with acknowledgement of others' ideas. He was generous in sharing his own ideas and seemed delighted when others would pick them up and carry them forward. I've always admired his openness and lack of jealousy in sharing ideas.

In his personal life, he seemed to have real compatibility with Lucy (his wife), who also kept him grounded. I still laugh when I remember once working with him at his dining room table and Lucy announcing, "Robin, enough of the mathematics. It's time to mow the lawn!"

I visited Oxford for Lucy's funeral and recall Robin putting a brave face on his future plans; I returned a few weeks later when Robin passed away himself. I miss him greatly. 

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!