This talk is about syntax, a typed syntax which captures diverse
classes of programming languages and computational behaviours,
of which I concentrate on sequential functional behaviour.
* * *
Capturing dynamics of programming languages formally by basic
syntax has started with, perhaps, the lambda-calculi (Landin
already noted this in 1960's). Later we found many related structures,
such as domains and CCCs, where the techniques and structures
developed around the lambda-calculi have always been fundamental.
The syntax and semantics can then be related nicely, e.g. as the
relationship between meta-languages of given semantic universes.
This was made possible by decomposing computational dynamics into
higher-order functions. This representation is surprisingly flexible
and powerful: an elementary example is the representation of memory
and assignment commands as certain higher-order functions. The
power of this decomposition lies at the heart of the expressiveness
of various universes of domains.
The pi-calculus can be considered as a tool which directly extends
this aspect of the lambda-calculus. Instead of using higher-order
functions, it decomposes computation into name-passing interaction
--- which is more fine-grained and powerful. Many people have
already shown embeddings of varied computational structures in
this calculus. These results are reminiscent of representation of
programming constructs using the lambda calculi, but often with
tighter operational correspondence.
Against this background, what I shall discuss in this talk is by adding
a very simple notion of types, we can do such an embedding in a
rather pleasant way --- the embedding is now fully abstract, capturing
all essential information in target computational forms, in this case the
behaviour of sequential higher-order functions. The typed syntax is
simple, while the resulting processes uniformly captures both
call-by-name and call-by-value sequential behaviour. We in
particular show a simple and fully abstract embedding of PCF in a
typed pi-calculus, which has a close connection to the AJM-HO
games introduced in 1994.
* * *
One way of seeing this result is that pi-calculus is now poised to
represent basic universes of (typed) lambda-calculi in a
satisfactory way, thus briding the world of lambda-calculi and the
world of pi-calculi (sequentiality is that bridge). This is a joint work
with Martin Berger and Nobuko Yoishida.