Open AccessObjects, Types and Modal Logics
Author(s) -
Dan S. Andersen,
Lars Pedersen,
Hans Hüttel,
Josva Kleist
Publication year - 1996
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v3i49.20051
Subject(s) - modal logic , modal , fragment (logic) , mathematics , translation (biology) , connection (principal bundle) , temporal logic , discrete mathematics , calculus (dental) , type (biology) , combinatorics , computer science , algorithm , programming language , geometry , chemistry , medicine , ecology , biochemistry , dentistry , biology , messenger rna , polymer chemistry , gene
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-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.