Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Kohei Honda
Kohei Honda
Email: kohei::@dcs.qmul.ac.uk
(please take off :: from the address: this is for preventing
spam)
Phone: +44 20 7882 5226
Fax: +44 181 980 6533
Room: 1431
Department of Computer Science
Queen Mary & Westfield College
Mild End Road
London E1 4NS
last update: March, 2007.
Recent news.
- 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
discussion (and
a chinese dish) there.
- April 2005, I have completed two papers on logic for imperative
higher-order
functions,
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
general software
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
software.
Not-so-recent events.
- -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
good
fish
meal).
- -Sept, 2002 I have been to Pisa to give a talk (and eat
Pizza and other delicious things, naturally...).
Research Interests.
- Basic theories of processes and its applications.
- Pi-calculus.
- More generally, science of computing and information from the
viewpoint of interaction.
For more details, see here .
Recent Papers
-- 
Nonintertference Proofs through Flow Analysis, with Nobuko Yoshida.
45pp.
The updated
version of an earlier short manuscript. The role of polarities
in flow analysis is clarified.
September 23, 2003 [ps-file]
and
[pdf-file]
-- Strong
Normalisability in the Pi-calculus (an updated full version)
Information and Computation,
with Martin Berger and
Nobuko
Yoshida. 55pp. August, 2003 [ps-file]
and
[pdf-file]
-- Genericity and the Pi-Calculus (short version)
with Martin Berger and Nobuko
Yoshida, 16pp. January 17.
FOSSACS'03.
[ps-file]
and
[pdf-file]
-- Genericity and the Pi-Calculus (full version)
with Martin Berger and Nobuko Yoshida,
66pp. November 15, 2002 [ps-file]
and
[pdf-file]
-- Uniform Type Structure for Secure Information Flow (full
version)
with Nobuko Yoshida, 72pp. August
2002 [ps-file] and
[pdf-file]
Papers
(1) On the representation of basic classes of computation using the
pi-calculus.
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
to Nobuko!
- Sequentiality and the Pi-calculus. with Martin
Berger and Nobuko Yoshida.
The short version will appear in TLCA'01. This paper
characterises theclass
of sequential higher-order computation without commitment to
specific
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,
rather simply,
the class of converging higher-order computation. [ps-file]
- Genericity and the Pi-calculus. with Martin Berger and
Nobuko Yoshida.
Duality leads to a nice theory of genericity. The short version [ps-file]
appeared in FOSSACS'03. The full version ] [ps-file]
contains more
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
each different
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
distributed
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
Nobuko Yoshida.
The initial version appeared in ESOP'00. How about
representing
a special kind of computational behaviour, such as a "secure" one? This
is an
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
timer.
- 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
Renaming.
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,
112 pages)
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!
[ps-file]
- Notes on Undirected Action Structures. Typescript,
May 1997.
[ps-file]
- Composing Processes. POPL'96, January 1996,
pp.344-357, ACM Press.
[ps-file]
- Process Structures. in Proc. of TPPP'94, LNCS
907, pp.25-44, 1995.
[ps-file]
(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.
- Processes and Games.
In WRLA 2002, ENTCS 71, 2004
[pdf-file]
- 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
abstract)
Kohei Honda and Nobuko Yoshida, In Proc. of ICALP'97, LNCS,
Springer-Verlag,
Bologna, Italy, July, 1997. [ps-file]
(5) The asynchronous version of the Pi-calculus. This gives a
basic form of name passing interaction,
and is the basis of the work
listed in (1). The formalism was also discovered independently by
Boudol
- 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
Mario Tokoro.
Object-Based Concurrent Computing, LNCS, Vol. 612, pp. 21-51,
Springer-Verlag, 1992.
[ps-file]
- Two bisimilarities in $\nu$-calculus.
Keio CS report 92-002, Department of Computer Science, Keio University,
1992.
[ps-file]
- On Reduction-Based Process Semantics: (extended
abstract)
Kohei Honda and Nobuko Yoshida, In Proc. of FST/TCS'13, LNCS
761, pp. 373-387,
Springer-Verlag, December, 1993.
[ps-file]
- 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.
[ps-file]
(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
Communication-based
Programming. with Vasco Vasconcelos and Makoto Kubo. In Proc.
of ESOP'98, LNCS,
Springer-Verlag, April, 1998. [ps-file] and
[pdf-file]
(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.
[ps-file]
[end]