** Next:** Programming Languages
**Up:** Logics for Concurrency and
** Previous:** Game semantics for the

In [AmCou97] Amadio and Coupet-Grimal consider the issue
of representing ``infinite'' and ``total'' objects like infinite
streams or non-terminating processes in type theory. They present a
realizability interpretation of co-inductive types based on *
partial equivalence relations* (per's), and extract from the per's
interpretation sound rules to type recursive definitions. These
recursive definitions are needed to introduce `infinite' objects of
co-inductive type. One can show that the proposed type system enjoys
the basic syntactic properties of subject reduction and strong
normalization with respect to a confluent rewriting system first
studied by Gimenez. The proposed type system is compared with those
by Coquand and Gimenez. In particular, it provides a semantic
reconstruction of Gimenez's system which suggests a rule to type
nested recursive definitions.

The final version of the book [AmCu97] has been delivered. The book addresses the mathematical aspects of the semantics of programming languages. The mathematical objects manipulated are order-theoretic structures, and the languages we consider are typed lambda-calculi. The book considers various extensions of typed lambda-calculi to include non-determinism, communication, and concurrency, and it summarizes some of the work carried on in the Confer project.

In [HaHen97e] Hartonas and Hennessy use traditional denotational
techniques to give a denotational model of a subset of *core
Facile* . Specifically this is applied typed call-by-value language
which in addition to the usual types has an extra type for processes,
which can exchange values along communication channels, a la
*CCS* . The model is shown to be fully-abstract with respect to a
version of *may testing* . It is notable that in order to achieve
full-abstraction it is necessary to add to the language an operator
which allows processes report the result of a computation.
[[Am97]]
R. Amadio.

An asynchronous model of locality, failure, and process mobility.

In *Proc. Coordination 97, Springer Lect. Notes in Comp. Sci.
1282*, 1997.

[[AmCou97]]
R. Amadio and S. Coupet-Grimal.

Analysis of a guard condition in type theory (preliminary report).

Technical Report TR 1997.245. Also RR-3300 INRIA, Université de
Provence (LIM), 1997.

[[AmCu97]]
R. Amadio and P.-L. Curien.
*Domains and Lambda-Calculi*.

Cambridge University Press.

To appear.

[[AmPra97]]
R. Amadio and S. Prasad.

Modelling IP mobility.

Technical Report TR 1997.244. Also RR-3301 INRIA, Université de
Provence (LIM), 1997.

[[HaHen97e]]
C. Hartonas and M. Hennessy.

Full abstractness for a functional/concurrent language with
higher-order value-passing.

Full version available as Computer Science Technical Report 1/97,
University of Sussex, 1997. Available from http://www.cogs.susx.ac.uk/.