Staged composition synthesis

Boris Düdder; Moritz Martens; Jakob Rehof

doi:10.1007/978-3-642-54833-8_5

Staged composition synthesis

Boris Düdder, Moritz Martens, Jakob Rehof

20 Citationer (Scopus)

Abstract

A framework for composition synthesis is provided in which metalanguage combinators are supported and the execution of synthesized programs can be staged into composition-time code generation (stage 1) and run-time execution (stage 2). By extending composition synthesis to encompass both object language (L1) and metalanguage (L2) combinators, composition synthesis becomes a powerful and flexible framework for the generation of L1-program compositions. A system of modal intersection types is introduced into a combinatory composition language to control the distinction between L1- and L2-combinators at the type level, thereby exposing the language distinction to composition synthesis. We provide a theory of correctness of the framework which ensures that generated compositions of component implementations are well typed and that their execution can be staged such that all metalanguage combinators can be computed away completely at stage 1, leaving only well typed L1-code for execution at stage 2. Our framework has been implemented, and we report on experiments.

Originalsprog	Engelsk
Titel	Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings
Antal sider	20
Forlag	Springer Verlag
Publikationsdato	1 jan. 2014
Sider	67-86
ISBN (Trykt)	9783642548321
DOI	https://doi.org/10.1007/978-3-642-54833-8_5
Status	Udgivet - 1 jan. 2014
Begivenhed	23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 - Grenoble, Frankrig Varighed: 5 apr. 2014 → 13 apr. 2014

Konference

Konference	23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
Land/Område	Frankrig
By	Grenoble
Periode	05/04/2014 → 13/04/2014
Sponsor	Université de Toulouse, Grenoble INP, Inria, PERSYVAL-Lab and Universite Joseph Fourier, Springer-Verlag

Navn	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind	8410 LNCS
ISSN	0302-9743

Adgang til dokumentet

10.1007/978-3-642-54833-8_5

Andre filer og links

Link to publication in Scopus

Citationsformater

Düdder, B., Martens, M., & Rehof, J. (2014). Staged composition synthesis. I Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings (s. 67-86). Springer Verlag. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Bind 8410 LNCS https://doi.org/10.1007/978-3-642-54833-8_5

Staged composition synthesis. / Düdder, Boris; Martens, Moritz; Rehof, Jakob.

Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag, 2014. s. 67-86 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 8410 LNCS).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Düdder, B, Martens, M & Rehof, J 2014, Staged composition synthesis. i Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 8410 LNCS, s. 67-86, 23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, Frankrig, 05/04/2014. https://doi.org/10.1007/978-3-642-54833-8_5

Düdder B, Martens M, Rehof J. Staged composition synthesis. I Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag. 2014. s. 67-86. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 8410 LNCS). doi: 10.1007/978-3-642-54833-8_5

Düdder, Boris ; Martens, Moritz ; Rehof, Jakob. / Staged composition synthesis. Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag, 2014. s. 67-86 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 8410 LNCS).

@inproceedings{a8e79a8b0f614765b30faa334b66d2c0,

title = "Staged composition synthesis",

abstract = "A framework for composition synthesis is provided in which metalanguage combinators are supported and the execution of synthesized programs can be staged into composition-time code generation (stage 1) and run-time execution (stage 2). By extending composition synthesis to encompass both object language (L1) and metalanguage (L2) combinators, composition synthesis becomes a powerful and flexible framework for the generation of L1-program compositions. A system of modal intersection types is introduced into a combinatory composition language to control the distinction between L1- and L2-combinators at the type level, thereby exposing the language distinction to composition synthesis. We provide a theory of correctness of the framework which ensures that generated compositions of component implementations are well typed and that their execution can be staged such that all metalanguage combinators can be computed away completely at stage 1, leaving only well typed L1-code for execution at stage 2. Our framework has been implemented, and we report on experiments.",

author = "Boris D{\"u}dder and Moritz Martens and Jakob Rehof",

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-642-54833-8_5",

language = "English",

isbn = "9783642548321",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "67--86",

booktitle = "Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings",

note = "23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 ; Conference date: 05-04-2014 Through 13-04-2014",

}

TY - GEN

T1 - Staged composition synthesis

AU - Düdder, Boris

AU - Martens, Moritz

AU - Rehof, Jakob

PY - 2014/1/1

Y1 - 2014/1/1

N2 - A framework for composition synthesis is provided in which metalanguage combinators are supported and the execution of synthesized programs can be staged into composition-time code generation (stage 1) and run-time execution (stage 2). By extending composition synthesis to encompass both object language (L1) and metalanguage (L2) combinators, composition synthesis becomes a powerful and flexible framework for the generation of L1-program compositions. A system of modal intersection types is introduced into a combinatory composition language to control the distinction between L1- and L2-combinators at the type level, thereby exposing the language distinction to composition synthesis. We provide a theory of correctness of the framework which ensures that generated compositions of component implementations are well typed and that their execution can be staged such that all metalanguage combinators can be computed away completely at stage 1, leaving only well typed L1-code for execution at stage 2. Our framework has been implemented, and we report on experiments.

AB - A framework for composition synthesis is provided in which metalanguage combinators are supported and the execution of synthesized programs can be staged into composition-time code generation (stage 1) and run-time execution (stage 2). By extending composition synthesis to encompass both object language (L1) and metalanguage (L2) combinators, composition synthesis becomes a powerful and flexible framework for the generation of L1-program compositions. A system of modal intersection types is introduced into a combinatory composition language to control the distinction between L1- and L2-combinators at the type level, thereby exposing the language distinction to composition synthesis. We provide a theory of correctness of the framework which ensures that generated compositions of component implementations are well typed and that their execution can be staged such that all metalanguage combinators can be computed away completely at stage 1, leaving only well typed L1-code for execution at stage 2. Our framework has been implemented, and we report on experiments.

UR - http://www.scopus.com/inward/record.url?scp=84900565033&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-54833-8_5

DO - 10.1007/978-3-642-54833-8_5

M3 - Article in proceedings

AN - SCOPUS:84900565033

SN - 9783642548321

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 67

EP - 86

BT - Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings

PB - Springer Verlag

T2 - 23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014

Y2 - 5 April 2014 through 13 April 2014

ER -

Staged composition synthesis

Abstract

Konference

Adgang til dokumentet

Andre filer og links

Fingeraftryk

Citationsformater