Kohei Honda succumbed to his recent illness and passed away on Monday 3rd December 2012.
Kohei's loss is a sad one for the School of Electronic Engineering and Computer Science. His work on Distributed Systems and the Ocean Observatories Project is something of which we were very proud.
We will all remember his enthusiasm for the subject.
There will be more information regarding his funeral and memorial available at http://www.eecs.qmul.ac.uk/KHmemorial/
Kohei Honda Email: kohei::@dcs.qmul.ac.uk
(please take off :: from the address: this is for preventing
Phone: +44 20 7882 5226
Fax: +44 181 980 6533
Department of Computer Science
& Westfield College
Mild End Road
London E1 4NS
last update: February 11, 2011.
latest DBLP entry is
Recent news. - April 15 2012: I am attending Milner
Symosium. It was in Paphos, Cyprus, March 2010,
that I learned of his abrupt death.
- February 11 2011: Having a great time in Bhubaneswar (KIIT/KISS), India. Has given a talk on
Scribble, here is the paper: [pdf] .
- (I admit no update has taken place for two years, anyway I add one recent news above)
- January 12 2009: Decided to update this homepage --- very soon.
- January 12 2009: Completing a long-due review of a long paper on pi-calculus.
- December 2008: A prototype "architecture" for session types completed by Ray.
- October 2008: A paper about "principal" session types with Dimitris and Nobuko (to appear in ESOP).
- July 2008. I was Reykjavik: and found people in Iceland eat just ordinary but delicious fishballs.
- June 2008. Here are some recent works, in case you are interested...
- June 2008. I was in Oslo and drank a glass of delicious water.
- A work on generalised session types [pdf] (Nobuko presented this in
San Francisco in January)
- A work on logics for the pi-calculus [pdf]
(presented in Reykjavik in July: a full version with all detailed proofs coming very soon)
- A work on SJ, a programming language for session types [pdf]
(Ray presented this in Cyprus in July)
- February 2007, I was in Paris and ate a heavenly tarte cake by Varia.
- July 2006. I was in Bertinoro. Before then, I was in Venice (giving two talks) and
then in a small village in Germany (giving one talk). I thought apples in Germany
were very very good, but later I found they were imported from Chile.
- March 2006, I visited Glasgow, had a very good discussion, and ate a marvelous
Peacan pie there.
- August 2005: Two modest works, one on sequential computation and
another on concurrent
one, are coming soon.
- June 2005, I visited Harvard, gave a talk, and had a very good
a chinese dish) there.
- April 2005, I have completed two papers on logic for imperative
done with Martin Berger and Nobuko Yoshida, one showing a
precise tie between
programs' behaviour and our program logic and another
presenting a simple and
general way to treat aliasing. These works, together with other
works on logics for
behaviour, are posted here.
The purpose of our work on logics is to obtain deeper
understanding of structures of software,
thus offering an effective basis of better engineering of
- -Sept, 2004 I have been to New York to give a talk and had a
great sushi there.
- -June, 2004 I have been to Edinburgh to give a talk (and had a
- -Sept, 2002 I have been to Pisa to give a talk (and eat
Pizza and other delicious things, naturally...).
- Basic theories of processes and its applications.
- More generally, science of computing and information from the
viewpoint of interaction.
For more details, see here .
Nonintertference Proofs through Flow Analysis, with Nobuko Yoshida.
version of an earlier short manuscript. The role of polarities
in flow analysis is clarified.
September 23, 2003 [ps-file]
Normalisability in the Pi-calculus (an updated full version)
Information and Computation,
-- Genericity and the Pi-Calculus (short version)
with Martin Berger and
Yoshida. 55pp. August, 2003 [ps-file]
with Martin Berger and Nobuko
Yoshida, 16pp. January 17.
-- Genericity and the Pi-Calculus (full version)
with Martin Berger and Nobuko Yoshida,
66pp. November 15, 2002 [ps-file]
-- Uniform Type Structure for Secure Information Flow (full
with Nobuko Yoshida, 72pp. August
2002 [ps-file] and
(1) On the representation of basic classes of computation using the
We have been accumulating basic results
as well as applications. We are
planning to start new research projects
in this context very soon. This field
of research has almost infinite
possibility, and if you are interested and able,
you deserve to do some of its most
interesting parts. If you are interested
please write to me or to Martin or
- Sequentiality and the Pi-calculus. with Martin
Berger and Nobuko Yoshida.
The short version will appear in TLCA'01. This paper
of sequential higher-order computation without commitment to
evaluation strategies. Done in December 2000. [ps-file]
- Strong Normalisation in the Pi-calculus. with
Martin Berger and Nobuko Yoshida.
The short version will appear in LICS'01. This paper characterises,
the class of converging higher-order computation. [ps-file]
- Genericity and the Pi-calculus. with Martin Berger and
Duality leads to a nice theory of genericity. The short version [ps-file]
appeared in FOSSACS'03. The full version ] [ps-file]
examples, comparisons and proofs.
- Linearity and Bisimulation. with Martin
Berger and Nobuko Yoshida.
It looks there is a new kind of bisimilarity methods popping up from
class of computational behaviours. This is one example. It gives
an equality for
a pure functional computation in the pi-calculus. What is interesting?
Well, it is the
pi-calculus, there is nothing like "pure" and "impure" here, so the
equality scales all
the way through to nondeterministic, nonfunctional, and even
computing... The short version appeared in FoSSacs'02. [ps-file]
- A uniform framework for secure information flow.
with Nobuko Yoshida.
This is a preliminary experiment of our theory to an area of security.
A short verision
is presented at POPL'02. This shows how we can recapture
functional and imperative
secrecy theory using typed pi-calculus. [ps-file]
- Secure Information Flow as Typed Process Behaviour
. with Vasco Vasconcelos and
The initial version appeared in ESOP'00. How about
a special kind of computational behaviour, such as a "secure" one? This
application of the theory of types for pi-calculus to the area of
security: it is also
a foundational inquiry into theory of information flow from the
viewpoint of processes
(a sequel to this paper deals with semantic aspects of this work and
will be posted
in this page shortly). [ps-file]
(2) Extending the Pi-calculus so that it can represent fundamental
elements of distributed
computing. This is a bit tough,
since we should identify a nice new primitive. So far
we (Martin) identified one: a
- Two-phase commitment protocol in an extended Pi-calculus
. with Martin Berger.
The short version appeared in Express'00, presenting a basic
theory of timer.
Done in October 2000. [ps-file]
(3) General Semantic theories underlying (1) and (2). Somehow nobody is
doing this kind,
except Milner and his group are
working on action structures and bigraphs, which are closely
related. These are hugely useful
when doing a basic study on processes.
- Elementary Structures for Process Theory (1): Sets with
March 1997, 37pp. MSCS, 2001. This is a rather general theory in
which most of the existing
syntactic theories of processes can be interpreted. [ps-file]
- A Theory of Types for the pi-calculus. (long version,
Typescript. November 7, 1998.
I found a strikingly nice theory
related to this: this will be incorporated in a new version I will be
working on soon!
- Notes on Undirected Action Structures. Typescript,
- Composing Processes. POPL'96, January 1996,
pp.344-357, ACM Press.
- Process Structures. in Proc. of TPPP'94, LNCS
907, pp.25-44, 1995.
(4) Game semantics. This has become a forerunner for the work in
(1). If you like the category
and the pi-calculus (which
is rare), you would like it. To process theorists: well, categories
are not so bad. First as a mental
gymnastics. Second as a way of organising semantic universes.
(5) The asynchronous version of the Pi-calculus. This gives a
basic form of name passing interaction,
- Processes and Games.
In WRLA 2002, ENTCS 71, 2004
- Recursive Types in Games: Axiomatics and Process
Representation. with Marcelo Fiore.
In LICS'98. [pdf-file]
- Fully Abstract Game Semantics for General Reference.
with Samson Abramsky and
Guy McCusker. In LICS'98. [ps-file]
- Game-theoretic Analysis of Call-by-value Computation: (newly
revised full version)
with Nobuko Yoshida, Feb 1997, revised October 1997. [ps-file]
- Game-theoretic Analysis of Call-by-Value Computation: (extended
Kohei Honda and Nobuko Yoshida, In Proc. of ICALP'97, LNCS,
Bologna, Italy, July, 1997. [ps-file]
and is the basis of the work
listed in (1). The formalism was also discovered independently by
- An Object Calculus for Asynchronous Communication. with
Mario Tokoro, Proc. of ECOOP'91
LNCS 512, pp.133-147, Springer-Verlag, 1991. Many questions posed here
have been answered,
but not all. [ps-file] and [pdf-file]
- On Asynchronous Communication Semantics, with
Object-Based Concurrent Computing, LNCS, Vol. 612, pp. 21-51,
- Two bisimilarities in $\nu$-calculus.
Keio CS report 92-002, Department of Computer Science, Keio University,
- On Reduction-Based Process Semantics: (extended
Kohei Honda and Nobuko Yoshida, In Proc. of FST/TCS'13, LNCS
761, pp. 373-387,
Springer-Verlag, December, 1993.
- Combinatory Representation of Mobile Processes. with
Nobuko Yoshida. POPL'94
ACM Press, 1994. [ps-file]
- Replication in Concurrent Combinators.
with NobukoYoshida. TACS'94, LNCS, 1994.
(6) Session types. Decomposing interaction structure into
asynchronous name passing gives you a new way to
abstract communication behaviours.
- An Interaction-based Language and its Typing System.
with Kaku Takeuchi and Makoto Kubo.
In Proc. of PARLE'94, LNCS 817, pp.398-413, Springer-Verlag, 1994. [ps-file]
- Language Primitives and Type Discipline for Structured
Programming. with Vasco Vasconcelos and Makoto Kubo. In Proc.
of ESOP'98, LNCS,
Springer-Verlag, April, 1998.
(7) Study of basic typing systems for the pi-calculus. These work
prepared the way towards my
study listed in (1).
- Principal typing schemes in a polyadic
pi-calculus. with Vasco Vasconcelos. CONCUR'93,
LNCS 715, pp. 524-538, Springer-Verlag, 1993. [ps-file]
- Types for dyadic Interaction. CONCUR'93,
LNCS 715, pp.509-523, Springer-Verlag, 1993.