Standard
Modal intersection types, two-level languages, and staged synthesis. / Henglein, Fritz; Rehof, Jakob.
Semantics, logics, and calculi: essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays. ed. / Chistian W. Probst; Chris Hankin; René Rydhof Hansen. Springer, 2016. p. 289-312 (Lecture notes in computer science, Vol. 9560).
Research output: Chapter in Book/Report/Conference proceeding › Book chapter › Research › peer-review
Harvard
Henglein, F & Rehof, J 2016,
Modal intersection types, two-level languages, and staged synthesis. in CW Probst, C Hankin & RR Hansen (eds),
Semantics, logics, and calculi: essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays. Springer, Lecture notes in computer science, vol. 9560, pp. 289-312.
https://doi.org/10.1007/978-3-319-27810-0_15
APA
Henglein, F., & Rehof, J. (2016).
Modal intersection types, two-level languages, and staged synthesis. In C. W. Probst, C. Hankin, & R. R. Hansen (Eds.),
Semantics, logics, and calculi: essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays (pp. 289-312). Springer. Lecture notes in computer science Vol. 9560
https://doi.org/10.1007/978-3-319-27810-0_15
Vancouver
Henglein F, Rehof J.
Modal intersection types, two-level languages, and staged synthesis. In Probst CW, Hankin C, Hansen RR, editors, Semantics, logics, and calculi: essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays. Springer. 2016. p. 289-312. (Lecture notes in computer science, Vol. 9560).
https://doi.org/10.1007/978-3-319-27810-0_15
Author
Henglein, Fritz ; Rehof, Jakob. / Modal intersection types, two-level languages, and staged synthesis. Semantics, logics, and calculi: essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays. editor / Chistian W. Probst ; Chris Hankin ; René Rydhof Hansen. Springer, 2016. pp. 289-312 (Lecture notes in computer science, Vol. 9560).
Bibtex
@inbook{18ecaf9324b1422387af82d19d4f55d2,
title = "Modal intersection types, two-level languages, and staged synthesis",
abstract = "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.",
author = "Fritz Henglein and Jakob Rehof",
note = "Nielsons' Festschrift",
year = "2016",
doi = "10.1007/978-3-319-27810-0_15",
language = "English",
isbn = "978-3-319-27809-4",
series = "Lecture notes in computer science",
publisher = "Springer",
pages = "289--312",
editor = "Probst, {Chistian W.} and Chris Hankin and Hansen, {Ren{\'e} Rydhof}",
booktitle = "Semantics, logics, and calculi",
address = "Switzerland",
}
RIS
TY - CHAP
T1 - Modal intersection types, two-level languages, and staged synthesis
AU - Henglein, Fritz
AU - Rehof, Jakob
N1 - Nielsons' Festschrift
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-319-27810-0_15
DO - 10.1007/978-3-319-27810-0_15
M3 - Book chapter
AN - SCOPUS:84955314125
SN - 978-3-319-27809-4
T3 - Lecture notes in computer science
SP - 289
EP - 312
BT - Semantics, logics, and calculi
A2 - Probst, Chistian W.
A2 - Hankin, Chris
A2 - Hansen, René Rydhof
PB - Springer
ER -
