Static interpretation of higher-order modules in Futhark: functional GPU programming in the large

Martin Elsman 1 Troels Henriksen 1 Danil Annenkov 2 Cosmin Oancea 1
1 DIKU - Department of computer Science [Copenhagen]
2 GALLINETTE - GALLINETTE
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
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 modules Semantics Modularity Parallel programming languages Modules / packages functional languages compilers Fomalisation Coq formal proof
Type de document :
Communication dans un congrès
ICFP 2018 - International Conference on Functional Programming, Sep 2018, St. Louis, United States. ACM, 2 (ICFP), pp.1-30, 2018, 〈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 : mercredi 3 octobre 2018 - 09:37:16

Fichier

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

Identifiants

Collections

UNIV-NANTES | LS2N-GALLINETTE | LS2N | UNAM | INRIA

Citation

Martin Elsman, Troels Henriksen, Danil Annenkov, Cosmin Oancea. Static interpretation of higher-order modules in Futhark: functional GPU programming in the large. ICFP 2018 - International Conference on Functional Programming, Sep 2018, St. Louis, United States. ACM, 2 (ICFP), pp.1-30, 2018, 〈10.1145/3236792〉. 〈hal-01883524〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

45

Téléchargements de fichiers

7

Contact


archive-ouverte@inria.fr