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

Elsman, M, Henriksen, T, Annenkov, D & Oancea, CE 2018, Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large. in Proceedings of the ACM on Programming Languages. ICFP edn, vol. 2, Association for Computing Machinery, pp. 97:1-97:30. https://doi.org/10.1145/3236792

APA

Elsman, M., Henriksen, T., Annenkov, D., & Oancea, C. E. (2018). Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large. In Proceedings of the ACM on Programming Languages (ICFP ed., Vol. 2, pp. 97:1-97:30). Association for Computing Machinery. https://doi.org/10.1145/3236792

Vancouver

Elsman M, Henriksen T, Annenkov D, Oancea CE. Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large. In Proceedings of the ACM on Programming Languages. ICFP ed. Vol. 2. Association for Computing Machinery. 2018. p. 97:1-97:30 https://doi.org/10.1145/3236792

Author

Elsman, Martin ; Henriksen, Troels ; Annenkov, Danil ; Oancea, Cosmin E. / Static Interpretation of Higher-order Modules in Futhark : Functional GPU Programming in the Large. Proceedings of the ACM on Programming Languages. Vol. 2 ICFP. ed. Association for Computing Machinery, 2018. pp. 97:1-97:30

Bibtex

@inproceedings{49559d10e0f94a2882d0279c87fe4a3e,
title = "Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large",
abstract = "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.",
keywords = "GPGPU, compilers, functional languages, modules",
author = "Martin Elsman and Troels Henriksen and Danil Annenkov and Oancea, {Cosmin E.}",
year = "2018",
doi = "10.1145/3236792",
language = "English",
volume = "2",
pages = "97:1--97:30",
booktitle = "Proceedings of the ACM on Programming Languages",
publisher = "Association for Computing Machinery",
edition = "ICFP",

}

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