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.
Type de document :
Article dans une revue
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (ICFP), pp.97:1--97:30. 〈10.1145/3236792〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01883524
Contributeur : Danil Annenkov <>
Soumis le : mardi 2 octobre 2018 - 13:44:36
Dernière modification le : mardi 26 mars 2019 - 09:25:22
Document(s) archivé(s) le : jeudi 3 janvier 2019 - 14:37:04

Fichier

ICFP18-modules.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Martin Elsman, Troels Henriksen, Danil Annenkov, Cosmin Oancea. Static interpretation of higher-order modules in Futhark: functional GPU programming in the large. Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (ICFP), pp.97:1--97:30. 〈10.1145/3236792〉. 〈hal-01883524〉

Partager

Métriques

Consultations de la notice

81

Téléchargements de fichiers

254