Static Interpretation of Higher-order Modules in Futhark: Functional GPU Programming in the Large
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
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 | 2018 |
Udgave | ICFP |
Sider | 97:1-97:30 |
DOI | |
Status | Udgivet - 2018 |
- GPGPU, compilers, functional languages, modules
Forskningsområder
ID: 218084789