Modal Functional (`Dialectica') Interpretation

We adapt our light Dialectica interpretation to usual and light modal formulas (with universal quantification on boolean and natural variables) and prove it sound for a non-standard modal arithmetic based on Goedel's T and classical S_4. The range of this light modal Dialectica is the usual (non-modal) classical Arithmetic in all finite types (with booleans); the propositional kernel of its domain is Boolean and not S_4. The `heavy' modal Dialectica interpretation is a new technique; it cannot be simulated within our previous light Dialectica. The synthesized functionals are at least as good as before; the translation process is much improved and could be more suitable for the human operators.