As mentioned in a previous post, Naoki Kobayashi will receive one of the two CONCUR 2026 Test-of-Time Awards at CONCUR 2026. Naoki has kindly agreed to answer some questions of mine on his award-winning paper via email. I am delighted to post his answers below and hope you'll enjoy reading them as much as I did. Thanks, Naoki!
Luca: You receive the CONCUR ToT Award 2026 for your paper A New Type System for Deadlock-Free Processes, which appeared at CONCUR 2006. That article is the culmination of a series of contributions you gave on the development of type systems for variations on the pi-calculus that guarantee deadlock-freedom. Could you briefly explain to our readers how you came to study the question addressed in your award-winning article and how the main ideas in your CONCUR 2006 paper evolved over time? Which of the ideas and results in your paper did you find most pleasing, surprising or challenging?
Naoki: If I remember correctly, the idea of using types to ensure deadlock-freedom came up during discussions on the linear pi-calculus with Benjamin Pierce and David Turner [1]. Indeed, if one wants to ensure that a channel is really used exactly once, one also has to ensure that the process does not get stuck before using it. An initial result on type systems for deadlock-freedom was published in LICS 1997 [2].
After that, the type system was extended in two directions: enabling automated type inference and increasing expressiveness. These were somewhat conflicting goals, and the CONCUR 2006 paper achieved a balance between them. The core idea was as follows. To ensure deadlock-freedom, it is necessary to control dependencies among different channels. In [2], such dependencies were expressed using “time tags” and a possibly infinite partial order on them. The time tags were later replaced by natural numbers, called capability and obligation levels, to enable automated inference [3], but at the cost of expressive power. The CONCUR 2006 paper combined a restricted form of time tags with capability and obligation levels, thereby recovering much of the expressive power while retaining automated inference.
What I found most pleasing was precisely this balance: the paper showed that one could make the type system significantly more practical without completely giving up the conceptual elegance and expressiveness of the earlier formulation.
[1] Naoki Kobayashi, Benjamin C. Pierce, David N. Turner, Linearity and the Pi-Calculus. POPL 1996: 358-37
[2] Naoki Kobayashi, A Partially Deadlock-Free Typed Process Calculus. LICS 1997: 128-139
[3] Naoki Kobayashi, Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4-5): 291-347 (2005)
After that, the type system was extended in two directions: enabling automated type inference and increasing expressiveness. These were somewhat conflicting goals, and the CONCUR 2006 paper achieved a balance between them. The core idea was as follows. To ensure deadlock-freedom, it is necessary to control dependencies among different channels. In [2], such dependencies were expressed using “time tags” and a possibly infinite partial order on them. The time tags were later replaced by natural numbers, called capability and obligation levels, to enable automated inference [3], but at the cost of expressive power. The CONCUR 2006 paper combined a restricted form of time tags with capability and obligation levels, thereby recovering much of the expressive power while retaining automated inference.
What I found most pleasing was precisely this balance: the paper showed that one could make the type system significantly more practical without completely giving up the conceptual elegance and expressiveness of the earlier formulation.
[1] Naoki Kobayashi, Benjamin C. Pierce, David N. Turner, Linearity and the Pi-Calculus. POPL 1996: 358-37
[2] Naoki Kobayashi, A Partially Deadlock-Free Typed Process Calculus. LICS 1997: 128-139
[3] Naoki Kobayashi, Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4-5): 291-347 (2005)
Luca: The contribution in your article achieves a good trade-off between expressiveness of the type system and ease of implementing its associated type inference algorithm. Did you or any other researcher try to extend the range of examples that could be handled by a variation on your type system? Do you think that it would be worth doing so or have we hit the point of diminishing returns, where any advance would be very technical and hard to implement?
Naoki: With Elena Giachino and Cosimo Laneve [4], I indeed investigated such an extension. The system developed there can deal with infinite chains of dependencies more general than those handled in the CONCUR 2006 paper. It was, however, developed for value-passing CCS rather than the pi-calculus. Incorporating the idea of [4] into the pi-calculus setting remains future work.
Another possible direction would be to combine the approach with generic types [5], which can capture precise dependencies among a set of channels. Unfortunately, I did not have time to fully explore this direction.As for whether it is worth pushing this line further, my feeling is that further general-purpose extensions may easily become technically involved and hard to implement. Perhaps a more promising direction would be to adapt the type system to real concurrent languages such as Go, and then see what kinds of extensions are most beneficial in practice.
[4] Elena Giachino, Naoki Kobayashi, Cosimo Laneve, Deadlock Analysis of Unbounded Process Networks. CONCUR 2014: 63-77
[5] Atsushi Igarashi, Naoki Kobayashi, A generic type system for the Pi-calculus. Theor. Comput. Sci. 311(1-3): 121-163 (2004)
Luca: Commendably, you supported the theoretical developments in your article with an implementation in TyPiCal. What role did the implementation work play in your research on type systems guaranteeing deadlock-freedom? Did the theoretical developments benefit from the implementation? Do you think that every proposal for a type system for some language ought to be accompanied by an implementation?
Naoki: TyPiCal was initially developed as a proof of concept for the type inference algorithm of [3]. At that time, the theory had already been fully developed, and the implementation was mainly used to convince readers that the algorithm indeed works in practice. In later extensions of TyPiCal, for the CONCUR 2006 paper and the work of [6], the implementation was also useful for checking the theories.
I think it is desirable for every type-system proposal to be accompanied by an implementation, although I would not say that it is absolutely necessary. An implementation is useful not only for checking the theory, but also for identifying limitations of the theory and suggesting possible directions for improvement.
[6] Naoki Kobayashi, Davide Sangiorgi, A Hybrid Type System for Lock-Freedom of Mobile Processes. CAV 2008: 80-93
Luca: In your paper, you showed, amongst other things, that the simply-typed λ-calculus with recursion could be encoded in the deadlock-free fragment of your calculus. What role did this result play in convincing you that your type system was sufficiently expressive? What were the main challenges that you had to overcome in developing that encoding and what were the main inspirations for that result?
Naoki: The encodability of the simply-typed λ-calculus with recursion in the deadlock-free fragment was a sort of minimal requirement for expressiveness. Since that property had already been shown for the original deadlock-free type system [2], I wanted to show that a similar level of expressive power was retained in the CONCUR 2006 type system.
There was also a more conceptual reason for considering such an encoding. Deadlock-freedom corresponds to the progress property of well-typed functional programs: evaluation does not get stuck. Thus, the encodability result shows that this progress property can be preserved by compilation from possibly parallel functional programs into the pi-calculus, which may be viewed as a CPS-style, lower-level language with concurrency primitives.
The main challenge was how to give a finite representation, within the type system, of the infinite chains of causal dependencies induced by recursion. As mentioned in the answer to the first question, we achieved this by combining the ideas of capability/obligation levels from [3] with a partial order on time tags from [2].
Luca: Your article gave a seminal contribution to the study of type systems for the pi-calculus that guarantee some desirable properties. Other examples of such contributions are, for instance, your paper with Davide Sangiorgi on a type system for lock-freedom or the paper by Yuxin Deng and Davide Sangiorgi on ensuring termination by typability amongst others. In hindsight, are there any relations amongst those contributions or ideas that underlie them and that can guide further developments in a systematic fashion?
Naoki: All three type systems you mentioned are related in that they control causal dependencies using natural numbers called “levels.” The type system for deadlock-freedom forbids cyclic dependencies, while the type systems for lock-freedom and termination forbid infinite chains of dependencies. The formulation of such reasoning through types, however, suffers from inherent limitations in expressive power.
To address this limitation, my paper with Davide Sangiorgi [7] suggested a new direction: combining syntactic typing rules with semantic ones. The latter can be discharged by resorting to model checkers, interactive theorem provers, or other verification tools, thereby complementing the limitations of type systems. I think this combination of type-based reasoning and semantic verification may provide a useful guide for further developments: types can capture common structural patterns, while semantic methods can handle cases that fall outside the reach of purely syntactic typing rules.
[7] Naoki Kobayashi, Davide Sangiorgi, A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst. 32(5): 16:1-16:49 (2010)
Luca: Are there any problems that you left open in your award-winning article that you'd still love to see solved?
Naoki: I would still like to see at least two directions explored further. First, increasing the expressiveness of the type system by integrating the ideas of [4] and [5], mentioned above, would probably be necessary to make the approach practical. Second, since the type-based approach is inherently incomplete, finding a smooth integration with other methods, such as model checking and interactive theorem proving, remains an important open problem, as suggested in [6].
Luca: How did the results and the techniques you developed in your award-winning paper influence your subsequent research? Is there any result obtained by other researchers that builds on, or is related to, your work and that you like in particular?
Naoki: A key ingredient of our type systems for deadlock-freedom is the notion of obligations and capabilities. An obligation of a send or receive operation describes the need to perform that operation, while a capability describes a guarantee that the operation can succeed. For example, in a client-server model, a client has the capability to send a request successfully, while a server has an obligation to receive and handle the request. In lock-based mutual exclusion, a thread has the capability to eventually acquire a lock, and, after acquiring the lock, it has an obligation to eventually release the lock.
These dual notions of obligations and capabilities turned out to be useful in other contexts. For example, we adapted them for automated verification of security protocols [8]. Another line of work developed related ideas for more conventional concurrent programming languages. Leino et al. [9] applied related techniques to deadlock-freedom of channels and locks, and this line was further extended to monitors and condition variables by Hamin and Jacobs [10]. I found this line of work particularly interesting because it shows that similar ideas arise naturally also in a more conventional programming-language setting.
[8] Morten Dahl, Naoki Kobayashi, Yunde Sun, Hans Hüttel, Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols. ATVA 2011: 75-89
[9] K. Rustan M. Leino, Peter Müller, Jan Smans, Deadlock-Free Channels and Locks. ESOP 2010: 407-426[10] Jafar Hamin, Bart Jacobs, Deadlock-Free Monitors. ESOP 2018: 415-441
Luca: What are the research topics related to type systems that you find most interesting right now? What role do you think type systems will or should have, if any, in the era of coding agents based on GenAI?
Naoki: I think GenAI may change not only type systems, but also the focus of formal methods more broadly. Traditionally, programs have been written by humans, and therefore “lightweight formal methods” have played an important role. In that setting, it was important to keep program annotations minimal and to automate verification or bug finding as much as possible, even if this sometimes came at the cost of precision or completeness.
In the era of GenAI-based coding agents, however, the situation may change. If coding agents can also generate annotations such as types and loop invariants, then the burden of writing annotations may no longer be such a serious issue. As a result, verification methods that aim at strong correctness guarantees, rather than merely finding bugs or checking lightweight properties, may become more important.
In this respect, the CONCUR 2006 type system can be seen as a product of the former design philosophy: it emphasized automation, at some cost in precision. A possible future direction would be to move beyond such lightweight type systems, by incorporating dependent types or combining type systems with other methods such as model checking, aiming at more complete verification methods.
Luca: What advice would you give to a young researcher who is keen to start working on topics related to types for programming languages?
Naoki: As discussed above, GenAI is rapidly changing the landscape of PL research, and we are facing significant challenges in adapting to these changes and finding new research directions to explore. I think this is a very good opportunity for “AI-native” young researchers to play important roles. My advice would be to learn the classical foundations carefully, but at the same time not to be constrained by traditional assumptions about how programs are written and verified.
