An Interpretation of Typed Objects Into Typed $pi$-calculusReport as inadecuate

An Interpretation of Typed Objects Into Typed $pi$-calculus - Download this document for free, or read online. Document in PDF available to download.

1 MEIJE - Concurrency, Synchronization and Real-time Programming CRISAM - Inria Sophia Antipolis - Méditerranée

Abstract : An interpretation of Abadi and Cardelli-s first-order functional {\em Object Calculus\-} \cite{AbCa94a} 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 \cite{PiSa93} - a development of Milner-s sorting discipline \cite{Mil91} with I-O annotations to separate the capabilities of reading and writing on a channel - but with {\em 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 ØbO languages.


Author: Davide Sangiorgi -



Related documents