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 IMT Atlantique - 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 : modules GPGPU Modules / packages functional languages compilers Semantics Coq formal proof Modularity Fomalisation Parallel programming languages
Document type :
Journal articles
Complete list of metadatas

Cited literature [52 references]  Display  Hide  Download
https://hal.inria.fr/hal-01883524
Contributor : Danil Annenkov <>
Submitted on : Tuesday, October 2, 2018 - 1:44:36 PM
Last modification on : Wednesday, January 22, 2020 - 2:52:07 PM
Long-term archiving on: Thursday, January 3, 2019 - 2:37:04 PM

File

ICFP18-modules.pdf
Files produced by the author(s)

Identifiers

Collections

UNIV-NANTES | LS2N-GALLINETTE | LS2N | UNAM | EC-NANTES | INRIA | CNRS | 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, ACM, 2018, 2 (ICFP), pp.97:1--97:30. ⟨10.1145/3236792⟩. ⟨hal-01883524⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

138

Files downloads

396

 

 

Contact

archive-ouverte@inria.fr