一句话：提出嵌入 F* 的依赖类型 GPU 编程语言 Kuiper，扩展分离逻辑以证明内核正确性并编译为高效 CUDA。
GPU 编程在追求高性能的同时难以保证安全与功能正确，且需处理内存层次、kernel 启动与同步等复杂细节。本文提出 Kuiper：一个作为可扩展库嵌入 F* 依赖类型语言的 CPU/GPU 编程语言。作者利用 F* 的依赖类型与 Pulse 并发分离逻辑，构建了一套程序逻辑，用于证明 CPU/GPU 程序安全、无数据竞争且功能正确。为刻画 GPU 的内存层次、kernel 启动与同步，他们扩展 Pulse，引入新的「定位资源」（located resources）概念与新连接词以结构化大规模并行推理，并给出新证明规则，将 GPU kernel 的逐线程视角提升为端到端正确性规约。Kuiper 提供高抽象层次的库，支持类型、操作、内存布局等多态，且不引入运行时开销，可编译为高效特化的 CUDA 代码，并支持一种新型的已验证 auto-tuning。实验表明，Kuiper 程序性能与手写 CUDA 相当，并与 cuBLAS 中闭源的最先进内核具有竞争力。
We introduce Kuiper, a language for safe and verified efficient CPU/GPU programming embedded as an extensible library within the F* dependently typed language. We rely on F*’s support for dependent types and its associated Pulse concurrent separation logic to develop a program logic in which to prove CPU/GPU programs safe, data-race free, and functionally correct. Our model of the GPU includes several intricacies, including the memory hierarchy, kernel launches, and synchronization within a single comprehensive framework. To do so, we extend the Pulse program logic with a novel notion of located resources and a new connective to structure reasoning about massively parallel programs, and present new proof rules to lift the per-thread view of GPU kernels to an end-to-end correctness specification. We have used Kuiper to program and prove correct a variety of GPU kernels, including full functional correctness proofs of an optimized matrix multiplication using two levels of block tiling and tensor cores. In doing so, we have developed a range of libraries to enable programs and proofs at a high level of abstraction but without imposing any runtime overhead. These allow Kuiper programs to be polymorphic (over types, operations, memory layout, and more) and compile to efficient, specialized CUDA code, while enabling a novel form of verified auto-tuning. Our experimental evaluation confirms that Kuiper programs match the performance of their handwritten CUDA counterparts and are competitive with closed source, state-of-the-art kernels in cuBLAS.
@article{MartinezKFERSSS26,
title = {Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic},
author = {Guido Martínez and Bastian Köpcke and Jonáš Fiala and Gabriel Ebner and Tahina Ramananandro and Michel Steuwer and Tyler Sorensen and Nikhil Swamy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808280}
}