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.

[end]