A typed λ-calculus, λ^{∩ ⎕}, is introduced, combining intersection types and modal types. We develop the metatheory of λ^{∩ ⎕}, with particular emphasis on the theory of subtyping and distributivity of the modal and intersection type operators. We describe how a stratification of λ^{∩ ⎕} leads to a multi-linguistic framework for staged program synthesis, where metaprograms are automatically synthesized which, when executed, generate code in a target language. We survey the basic theory of staged synthesis and illustrate by example how a two-level language theory specialized from λ^{∩ ⎕} can be used to understand the process of staged synthesis.