Objects, Types and Modal Logics

Dan S. Andersen
Lars H. Pedersen
Hans Hüttel
Josva Kleist

December 1996


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 tex2html_wrap_inline23 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 tex2html_wrap_inline23

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.