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

Martin Elsman; Troels Henriksen; Danil Annenkov; Cosmin E. Oancea

doi:10.1145/3236792

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

Martin Elsman, Troels Henriksen, Danil Annenkov, Cosmin E. Oancea

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.

Originalsprog	Engelsk
Titel	Proceedings of the ACM on Programming Languages
Antal sider	30
Vol/bind	2
Forlag	Association for Computing Machinery
Publikationsdato	sep. 2018
Udgave	ICFP
Sider	97:1-97:30
DOI	https://doi.org/10.1145/3236792
Status	Udgivet - sep. 2018

Emneord

GPGPU, compilers, functional languages, modules

Adgang til dokumentet

10.1145/3236792

http://dl.acm.org/ft_gateway.cfm?id=3236792&type=pdf

Citationsformater

Static Interpretation of Higher-order Modules in Futhark : Functional GPU Programming in the Large. / Elsman, Martin ; Henriksen, Troels; Annenkov, Danil et al.

Proceedings of the ACM on Programming Languages. Bind 2 ICFP. udg. Association for Computing Machinery, 2018. s. 97:1-97:30.

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

@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",

month = sep,

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",

}

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

Y1 - 2018/9

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 -

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

Abstract

Emneord

Adgang til dokumentet

Fingeraftryk

Citationsformater