Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-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.

In: Proceedings of the ACM on Programming Languages , Vol. 2, No. ICFP, 97, 01.07.2018.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-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', Proceedings of the ACM on Programming Languages , vol. 2, no. ICFP, 97. 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. Proceedings of the ACM on Programming Languages , 2(ICFP), [97]. https://doi.org/10.1145/3236792

CBE

Elsman M, Henriksen T, Annenkov D, Oancea CE. 2018. Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large. Proceedings of the ACM on Programming Languages . 2(ICFP):Article 97. https://doi.org/10.1145/3236792

MLA

Elsman, Martin et al. "Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large". Proceedings of the ACM on Programming Languages . 2018. 2(ICFP). 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. Proceedings of the ACM on Programming Languages . 2018 Jul 1;2(ICFP). 97. 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. In: Proceedings of the ACM on Programming Languages . 2018 ; Vol. 2, No. ICFP.

Bibtex

@article{8a3247fbbd7d426c90e8eea30686722e,
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, parallel programming, module systems, Coq, TYPED LAMBDA-CALCULUS, NORMALIZATION, compilers, modules, GPGPU, functional languages",
author = "Martin Elsman and Troels Henriksen and Danil Annenkov and Oancea, {Cosmin E.}",
year = "2018",
month = jul,
day = "1",
doi = "10.1145/3236792",
language = "English",
volume = "2",
journal = "Proceedings of the ACM on Programming Languages ",
issn = "2475-1421",
publisher = "ACM",
number = "ICFP",

}

RIS

TY - JOUR

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/7/1

Y1 - 2018/7/1

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

KW - parallel programming, module systems, Coq

KW - TYPED LAMBDA-CALCULUS

KW - NORMALIZATION

KW - compilers

KW - modules

KW - GPGPU

KW - functional languages

U2 - 10.1145/3236792

DO - 10.1145/3236792

M3 - Journal article

VL - 2

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - ICFP

M1 - 97

ER -