Options
2016
Conference Paper
Titel
Modal Intersection Types, Two-Level Languages, and Staged Synthesis
Abstract
A typed l-calculus, l∩⎕, is introduced, combining intersection types and modal types. We develop the metatheory of l∩⎕, with particular emphasis on the theory of subtyping and distributivity of the modal and intersection type operators. We describe how a stratification of l∩⎕ 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 l∩⎕ can be used to understand the process of staged synthesis.