| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [52 references]
https://hal.inria.fr/hal-01883524
Contributor : Danil Annenkov <>
Submitted on : Tuesday, October 2, 2018 - 1:44:36 PM
Last modification on : Thursday, February 27, 2020 - 1:10:41 AM
Document(s) archivé(s) le : Thursday, January 3, 2019 - 2:37:04 PM
Contributor : Danil Annenkov <>
Submitted on : Tuesday, October 2, 2018 - 1:44:36 PM
Last modification on : Thursday, February 27, 2020 - 1:10:41 AM
Document(s) archivé(s) le : Thursday, January 3, 2019 - 2:37:04 PM
File
ICFP18-modules.pdf
Files produced by the author(s)