Programming Languages

New submissions

• New submissions
• Replacements

New submissions for Thu, 9 May 24

[1]  arXiv:2405.04612 [pdf, ps, other]

Title: Numerical Fuzz: A Type System for Rounding Error Analysis

Authors: Ariel E. Kellison, Justin Hsu

Subjects: Programming Languages (cs.PL); Numerical Analysis (math.NA)

Algorithms operating on real numbers are implemented as floating-point computations in practice, but floating-point operations introduce roundoff errors that can degrade the accuracy of the result. We propose $\Lambda_{num}$, a functional programming language with a type system that can express quantitative bounds on roundoff error. Our type system combines a sensitivity analysis, enforced through a linear typing discipline, with a novel graded monad to track the accumulation of roundoff errors. We prove that our type system is sound by relating the denotational semantics of our language to the exact and floating-point operational semantics. To demonstrate our system, we instantiate $\Lambda_{num}$ with error metrics proposed in the numerical analysis literature and we show how to incorporate rounding operations that faithfully model aspects of the IEEE 754 floating-point standard. To show that $\Lambda_{num}$ can be a useful tool for automated error analysis, we develop a prototype implementation for $\Lambda_{num}$ that infers error bounds that are competitive with existing tools, while often running significantly faster. Finally, we consider semantic extensions of our graded monad to bound error under more complex rounding behaviors, such as non-deterministic and randomized rounding.

[2]  arXiv:2405.05118 [pdf, other]

Title: Full Version: (De/Re)-Composition of Data-Parallel Computations via Multi-Dimensional Homomorphisms

Authors: Ari Rasch

Comments: A short version of this paper is published at ACM TOPLAS

Subjects: Programming Languages (cs.PL)

We formally introduce a systematic (de/re)-composition approach, based on the algebraic formalism of "Multi-Dimensional Homomorphisms (MDHs)". Our approach is designed as general enough to be applicable to a wide range of data-parallel computations and for various kinds of target parallel architectures. To efficiently target the deep and complex memory and core hierarchies of contemporary architectures, we exploit our introduced (de/re)-composition approach for a correct-by-construction, parametrized cache blocking and parallelization strategy. We show that our approach is powerful enough to express, in the same formalism, the (de/re)-composition strategies of different classes of state-of-the-art approaches (scheduling-based, polyhedral, etc), and we demonstrate that the parameters of our strategies enable systematically generating code that can be fully automatically optimized (auto-tuned) for the particular target architecture and characteristics of the input and output data (e.g., their sizes and memory layouts). Particularly, our experiments confirm that via auto-tuning, we achieve higher performance than state-of-the-art approaches, including hand-optimized solutions provided by vendors (such as NVIDIA cuBLAS/cuDNN and Intel oneMKL/oneDNN), on real-world data sets and for a variety of data-parallel computations, including: linear algebra routines, stencil and quantum chemistry computations, data mining algorithms, and computations that recently gained high attention due to their relevance for deep learning.

Replacements for Thu, 9 May 24

[3]  arXiv:2203.00362 (replaced) [pdf, ps, other]

Title: Reasonable Space for the $λ$-Calculus, Logarithmically

Authors: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC); Programming Languages (cs.PL)

[4]  arXiv:2306.16330 (replaced) [pdf, ps, other]

Title: Proving Confluence in the Confluence Framework with CONFident

Authors: Raúl Gutiérrez, Salvador Lucas, Miguel Vítores

Comments: Extended and revised version of our LOPSTR 2022 paper (this https URL)

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

• New submissions
• Replacements