<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="7.x">Drupal-Biblio</source-app><ref-type>17</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Primiero, Giuseppe</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">A modal language for contextual computations</style></title></titles><dates><year><style  face="normal" font="default" size="100%">2007</style></year><pub-dates><date><style  face="normal" font="default" size="100%">June</style></date></pub-dates></dates><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;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 &lt;em&gt;unverified&lt;/em&gt; 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 &lt;em&gt;c&lt;/em&gt;ΚΤ&lt;sub&gt;⋄&lt;/sub&gt; 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..&lt;/p&gt;</style></abstract></record></records></xml>