Objects, Types and Modal Logics - Andersen, Dan S.; Pedersen, Lars H.; Hüttel, Hans; Kleist, Josva (BRICS Report Series, 1996)
In this paper we present a modal logic for describing properties of terms in the object calculus of Abadi and Cardelli [AC96]. The logic is essentially the modal mu-calculus of [Koz83]. The fragment allows us to express the temporal modalities of the logic CTL [BAMP83]. We investigate the connection between the type system Ob_1<:mu 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_1<:mu.