Modal intersection types, two-level languages, and staged synthesis

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

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.

Original languageEnglish
Title of host publicationSemantics, logics, and calculi : essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays
EditorsChistian W. Probst, Chris Hankin, René Rydhof Hansen
Number of pages24
PublisherSpringer
Publication date2016
Pages289-312
Chapter15
ISBN (Print)978-3-319-27809-4
ISBN (Electronic)978-3-319-27810-0
DOIs
Publication statusPublished - 2016
SeriesLecture notes in computer science
Volume9560
ISSN0302-9743

Bibliographical note

Nielsons' Festschrift

ID: 162646502