%0 Journal Article %D 2007 %T A modal language for contextual computations %A Primiero, Giuseppe %X

In this paper, we present a modal language for contextual computing, corresponding to the fragment of constructive ΚΤ with necessity and pos- sibility operators. We interpret absolute and contextual computations as difierent modes of verifying the truth of propositions. The semantics of the language L cc interprets absolute computations by a direct verification function valid in every state; contextual computations are interpreted in terms of a verification function valid under unverified information. Modal- ities are used to express extensions of contexts in order to de ne local and global validity. This semantics has a (weak) monotonicity property, de- pending on satisfaction of processes in contexts. In the corresponding axiomatic system cΚΤ a restricted version of the deduction theorem for globally valid formulas holds, soundness and completeness are proven and decidability is shown to hold for the necessitation fragment of the language by a restricted finite model property..

%8 June %G eng