A modal type theory for formalizing trusted communications (Q420842)

A multi-modal polymorphic type theory is introduced to model epistemic processes characterized by trust. Trust is defined as a second-order relation affecting the communication process between sources and a receiver. In the proposed language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgment. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version of a type theory, in which the modal operators are embedded into standard group knowledge operators.