[Prev][Next][Index][Thread]
paper available on typed pi-calculus and objects
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The paper below is now availabile from
http://cma.cma.fr:80/Personnel/Davide/recent.html
as piOCtyped.ps.gz.
Best regards,
Davide Sangiorgi
***********
Title: An interpretation of Typed Objects into Typed pi-calculus
Author: Davide Sangiorgi
note: INRIA Technical Report RR-3000.
Abstract: An interpretation of Abadi and Cardelli's first-order
functional *Object Calculus* into a typed pi-calculus is presented.
The interpretation validates the subtyping relation and the typing
judgements of the Object Calculus, and is computationally adequate.
The type language for the pi-calculus is that in
(Pierce-Sangiorgi,1993) --- a development of Milner's sorting
discipline with I/O annotations to separate the capabilities of
reading and writing on a channel --- but with *variants* in place of
tuples. Types are necessary to justify certain algebraic laws for
the pi-calculus which are important in the proof of computational
adequacy of the translation.
The study intends to offer a contribution to understanding, on the
one hand, the relationship between pi-calculus types and
conventional types of programming languages and, on the other hand,
the usefulness of the pi-calculus as a metalanguage for the
semantics of typed Object-Oriented languages.