Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Modal Intersection Types, Two-Level Languages, and Staged Synthesis

: Henglein, F.; Rehof, J.


Probst, C.W.:
Semantics, Logics, and Calculi : Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
Cham: Springer International Publishing, 2016 (Lecture Notes in Computer Science 9560)
ISBN: 978-3-319-27810-0
ISBN: 978-3-319-27809-4
International Conference on Semantics, Logics, and Calculi <2016, Lyngby>
Conference Paper
Fraunhofer ISST ()

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.