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.

Original language	English
Title of host publication	Proceedings of the ACM on Programming Languages
Number of pages	30
Volume	2
Publisher	Association for Computing Machinery
Publication date	Sept 2018
Edition	ICFP
Pages	97:1-97:30
DOIs	https://doi.org/10.1145/3236792
Publication status	Published - Sept 2018

Access to Document

10.1145/3236792

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

Cite this

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. 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

@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

Access to Document

Fingerprint

Cite this