Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Static Interpretation of Higher-order Modules in Futhark : Functional GPU Programming in the Large. / Elsman, Martin; Henriksen, Troels; Annenkov, Danil; Oancea, Cosmin E.
Proceedings of the ACM on Programming Languages. Vol. 2 ICFP. ed. Association for Computing Machinery, 2018. p. 97:1-97:30.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Static Interpretation of Higher-order Modules in Futhark
T2 - Functional GPU Programming in the Large
AU - Elsman, Martin
AU - Henriksen, Troels
AU - Annenkov, Danil
AU - Oancea, Cosmin E.
PY - 2018
Y1 - 2018
N2 - We present a higher-order module system for the purely functional data-parallel array language Futhark. The module language has the property that it is completely eliminated at compile time, yet it serves as a powerful tool for organizing libraries and complete programs. The presentation includes a static and a dynamic semantics for the language in terms of, respectively, a static type system and a provably terminating elaboration of terms into terms of an underlying target language. The development is formalised in Coq using a novel encoding of semantic objects based on products, sets, and finite maps. The module language features a unified treatment of module type abstraction and core language polymorphism and is rich enough for expressing practical forms of module composition.
AB - We present a higher-order module system for the purely functional data-parallel array language Futhark. The module language has the property that it is completely eliminated at compile time, yet it serves as a powerful tool for organizing libraries and complete programs. The presentation includes a static and a dynamic semantics for the language in terms of, respectively, a static type system and a provably terminating elaboration of terms into terms of an underlying target language. The development is formalised in Coq using a novel encoding of semantic objects based on products, sets, and finite maps. The module language features a unified treatment of module type abstraction and core language polymorphism and is rich enough for expressing practical forms of module composition.
KW - GPGPU, compilers, functional languages, modules
U2 - 10.1145/3236792
DO - 10.1145/3236792
M3 - Article in proceedings
VL - 2
SP - 97:1-97:30
BT - Proceedings of the ACM on Programming Languages
PB - Association for Computing Machinery
ER -
ID: 218084789