Abstract:
In this paper we present a modal logic for describing properties of terms
in the object calculus of Abadi and Cardelli. The logic is essentially
the modal mu-calculus. The fragment allows us to express the temporal
modalities of the logic CTL. We investigate the connection between the
type system Ob 
and the mu-calculus, providing a
translation of types into modal formulae and an ordering on formulae that
is sound w.r.t. to the subtype ordering of Ob
Available as PostScript, PDF, DVI.