FU Berlin, Fachbereich Mathematik und Informatik, Institut für Informatik

Vortrag des Informatik-Kolloquiums

We investigate the applicability of techniques known from the world of process calculi to reason about properties of object-oriented programs.

The investigation is performed upon a small object-oriented language --- The sigma-calculus of Abadi and Cardelli. The investigation is twofold:

• We investigate translations of sigma-calculi into process calculi, with the idea that one should be able to show properties of sigma-calculus programs by showing properties about their translations. We present translations of two sigma-calculi into pi-calculi. A translation of the untyped functional sigma-calculus turns out to be insufficient. Based on our experiences, we present a translation of a typed imperative sigma-calculus, which looks promising. We are able to provide simple proofs of the equivalence of different sigma-calculus objects using this translation.
• We use a labelled transition system adapted to the sigma-calculus to investigate the use of process calculi techniques directly on the sigma-calculus. The results obtained are of a fairly theoretical nature. We investigate the connection between the operational and denotational semantics for a typed functional sigma-calculus. The result is that Abadi and Cardelli's denotational model is sound but not complete with respect to the operational semantics. We also construct a modal logic for the typed functional sigma-calculus, provide a translation of types to a sub-logic and prove the translation is sound and complete.