Denotational semantics

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/.