An Interpretation of Typed Objects Into Typed $pi$-calculusReportar como inadecuado

An Interpretation of Typed Objects Into Typed $pi$-calculus - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.


Autor: Davide Sangiorgi -



Documentos relacionados