A Type Safe Translation of a Functional Array Language to a Process Calculus
Authors
Walsted, Loke ; Kleist, Daniel Vang
Term
4. term
Education
Publication year
2025
Submitted on
2025-06-06
Pages
41
Abstract
Graphics processing units (GPUs) can run many operations in parallel, whereas central processing units (CPUs) handle fewer tasks at a time. Futhark is a functional array programming language that uses high-level array operations called second-order array combinators (SOACs) to compile to efficient GPU code. This thesis extends an untyped core language, ButF (a subset of Futhark), and an extended pi-calculus with broadcasting, Epi (by Hüttel et al.), with simple type systems. The typed versions are called BtF and Tepi. We prove that both type systems are sound with respect to their semantics—that is, the typing rules align with the meaning of the languages and provide static guarantees about program behavior. We then extend the existing translation from ButF to Epi by incorporating these types, yielding a type-preserving, data-parallel implementation of BtF in Tepi. Finally, we prove the translation correct by showing that both types and behavior are preserved.
Grafiske processorer (GPU'er) kan udføre mange operationer samtidig, mens centrale processorer (CPU'er) typisk håndterer færre opgaver ad gangen. Futhark er et funktionelt arraysprog, der bruger højniveau-arrayoperationer kaldet second-order array combinators (SOACs) til at kompilere til effektiv GPU-kode. I dette arbejde udvider vi et utypet kernesprog, ButF (en delmængde af Futhark), og en udvidet pi-kalkyle med udsendelse, Epi (af Hüttel m.fl.), med simple typesystemer. De typede versioner kaldes BtF og Tepi. Vi beviser, at begge typesystemer er korrekte i forhold til deres semantik—dvs. at typereglerne stemmer overens med sprogenes betydning og giver statiske garantier for programadfærd. Dernæst udvider vi den eksisterende oversættelse fra ButF til Epi ved at indarbejde disse typer, hvilket giver en typebevarende, dataparallel implementering af BtF i Tepi. Til sidst beviser vi, at oversættelsen er korrekt, ved at vise, at både typer og adfærd bevares.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords
Type system ; Semantics ; Pi-calculus ; Futhark ; Encoding