For the mapping between the modally extended syntactic source calculus and the semantic target calculus LP, we have two options.  The first is to treat ◊,□ purely as syntactic control devices.  One then sets (◊A)′ = (□A)′ = A′, and the inference rules affecting the modalities leave no trace in the LP term associated with a derivation. The second is to actually provide denotation domains for the new types, and to extend the term language accordingly.  For the minimal logic of ◊,□, one can turn to Wansing (2002), who develops a set-theoretic interpretation of minimal temporal intuitionistic logic.  The temporal modalities of future possibility and past necessity are indistinguishable from the control operators ◊,□, prooftheoretically and as far as their relational interpretation is concerned.  Morrill (1990) gives an interpretation in intensional lambda calculus for a stronger S5 modality, which assumes a universal accessibility relation at the level of the frame semantics.  Denotations for modalized formulas A, in this setting, are functions from indices (situations, reference points) to A denotations.