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

International audienceWe 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 asa powerful tool for organizing libraries and complete programs. The presentation includes a static and adynamic semantics for the language in terms of, respectively, a static type system and a provably terminatingelaboration of terms into terms of an underlying target language. The development is formalised in Coqusing a novel encoding of semantic objects based on products, sets, and finite maps. The module languagefeatures a unified treatment of module type abstraction and core language polymorphism and is rich enoughfor expressing practical forms of module composition