An Interpretation of Typed Objects Into Typed $\pi$-calculus

Davide Sangiorgi 1
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.
Type de document :
RR-3000, INRIA. 1996
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:33:14
Dernière modification le : jeudi 11 janvier 2018 - 16:41:51
Document(s) archivé(s) le : dimanche 4 avril 2010 - 22:05:47



  • HAL Id : inria-00073696, version 1



Davide Sangiorgi. An Interpretation of Typed Objects Into Typed $\pi$-calculus. RR-3000, INRIA. 1996. 〈inria-00073696〉



Consultations de la notice


Téléchargements de fichiers