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

Martin Elsman 1 Troels Henriksen 1 Danil Annenkov 2, 3 Cosmin Oancea 1
1 DIKU - Department of computer Science [Copenhagen]
2 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
3 DAPI - Département Automatique, productique et informatique
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 : Coq formal proof GPGPU modules Semantics Modularity Parallel programming languages Modules / packages functional languages compilers Fomalisation
Type de document :
Communication dans un congrès
Proceedings of the ACM on Programming Languages, Sep 2018, St. Louis, United States. ACM, 2 (ICFP), pp.97:1--97: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 : mardi 22 janvier 2019 - 11:21:23
Document(s) archivé(s) le : jeudi 3 janvier 2019 - 14:37:04

Fichier

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

Identifiants

Collections

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

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, Sep 2018, St. Louis, United States. ACM, 2 (ICFP), pp.97:1--97:30, 2018, 〈10.1145/3236792〉. 〈hal-01883524〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

64

Téléchargements de fichiers

79

Contact


archive-ouverte@inria.fr