一句话：提出以 destination 为核心的纯函数式线性 λ-演算，用模态类型管理线性与作用域，并在 Coq 中证明类型安全。
目标传递（destination passing）又称 out 参数，即传入一个待填充的参数而非由函数返回结果；由于其表面上的命令式特征，它一直难以融入纯函数式编程。本文提出一种以目标（destination）为核心的纯函数式演算，统一并涵盖已有类似系统，可用于推理其正确性或扩展。该演算采用模态类型系统，借助 mode 同时管理线性与作用域，从而保证安全并表达此前未知可在纯语言中表达的程序。作者在 Coq 证明助手中形式化证明了核心演算的类型安全性。
Destination passing —aka. out parameters— is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional programming. In this paper, we present a pure functional calculus with destinations at its core. Our calculus subsumes all the similar systems, and can be used to reason about their correctness or extension. In addition, our calculus can express programs that were previously not known to be expressible in a pure language. This is guaranteed by a modal type system where modes are used to manage both linearity and scopes. Type safety of our core calculus was proved formally with the Coq proof assistant.
@article{paperbot3170,
title = {Destination Calculus: A Linear 𝜆-Calculus for Purely Functional Memory Writes},
author = {Thomas Bagrel and Arnaud Spiwack},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720423}
}