Modal intersection types, two-level languages, and staged synthesis
Research output: Chapter in Book/Report/Conference proceeding › Book chapter › Research › peer-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 language | English |
---|---|
Title of host publication | Semantics, logics, and calculi : essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays |
Editors | Chistian W. Probst, Chris Hankin, René Rydhof Hansen |
Number of pages | 24 |
Publisher | Springer |
Publication date | 2016 |
Pages | 289-312 |
Chapter | 15 |
ISBN (Print) | 978-3-319-27809-4 |
ISBN (Electronic) | 978-3-319-27810-0 |
DOIs | |
Publication status | Published - 2016 |
Series | Lecture notes in computer science |
---|---|
Volume | 9560 |
ISSN | 0302-9743 |
Bibliographical note
Nielsons' Festschrift
ID: 162646502