paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A theory of RPC calculi for client–server model

面向客户端–服务器模型的 RPC 演算理论
JFP vol.292019匹配度 2/10 · 论文属于多级编程/RPC 演算与类型系统的纯 PL 理论研究,未涉及 LLM/Agent、静态分析、浮点分析或贝叶斯程序分析,与画像核心方向没有直接交集;仅在形式化与类型系统层面与 PL 背景轻微相关。引用 10 inbox
KWANGHOON CHOI, BYEONG-MO CHANG
crossref: 2026-09-10

AI 速览

一句话:提出有状态 RPC 演算与位置类型系统,在编程视角支持对称通信、实现采用非对称通信,并统一三种服务器策略。

多级编程语言允许程序员标注代码运行位置,以简化客户端–服务器 Web 应用开发。现有 RPC 演算虽能在程序书写层面提供对称通信,并在 trampolined 风格下以非对称通信实现,但只考虑无状态服务器策略:它把服务器状态编码后传给客户端,因而无法正确处理涉及磁盘或数据库的有状态操作。本文提出有状态 RPC 演算,同时保留程序员视角的对称通信与实现层非对称通信;其核心是新的位置类型系统,为客户端–服务器模型的 RPC 演算理论奠定基础。该理论还能改进无状态策略,构造状态编码演算以消除远程过程调用中的运行时检查,并设计混合策略以兼取两类策略之长。作者声称这是首个在三种策略下同时提供对称通信书写与非对称通信实现的有类型多级演算。

问题
现有 RPC 演算仅支持无状态服务器策略,无法正确处理磁盘或数据库等有状态操作;已有工作要么只支持非对称通信,要么只适合点对点模型的对称实现。
方法
提出新的有状态 RPC 演算,基于新的位置类型系统设计有状态服务器策略,并用 trampolined 风格实现非对称通信;进而改进无状态策略并设计混合策略。
评估
通过演算定义、类型系统与策略比较进行理论论证,说明三种服务器策略可统一支持对称通信与非对称实现,并能消除远程调用的运行时检查。
原文摘要(Abstract)

Abstract With multi-tier programming languages, programmers can specify the locations of code to run in order to reduce development efforts for the web-based client–server model where programmers write client and server programs separately and test the multiple programs together. The RPC calculus, one of the foundations of those languages by Cooper and Wadler, has the feature of symmetric communication in programmer’s writing arbitrarily deep nested client–server interactions. The feature of the calculus is fully implemented by asymmetric communication in trampolined style suitable for the client–server model. However, the existing research only considers a stateless server strategy in which all server states are encoded for transmission to the client so that server states do not need to be stored in the server. It cannot always correctly handle all stateful operations involving disks or databases. To resolve this problem, we first propose new stateful calculi that fully support both symmetric communication from the programmer’s viewpoint and asymmetric communication in its implementation using trampolined style. All the existing calculi either provide only the feature of asymmetric communication or propose only symmetric implementation suitable for the peer-to-peer model, rather than the client–server model. Second, the method used to design our stateful server strategy is based on a new locative type system which paves the way for a theory of RPC calculi for the client–server model. Besides proposing the new stateful calculi, this theory can improve the existing stateless server strategy to construct new state-encoding calculi that eliminate runtime checks on remote procedure calls present in the existing strategy, and it enables us to design a new mixed strategy that combines the benefits of both kinds of strategies. As far as we know, there are no typed multi-tier calculi that offer programmers the feature of symmetric communication with the implementation of asymmetric communication under the three strategies together.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot728,
  title = {A theory of RPC calculi for client–server model},
  author = {KWANGHOON CHOI and BYEONG-MO CHANG},
  journal = {Journal of Functional Programming},
  volume = {29},
  year = {2019},
  doi = {10.1017/s0956796819000029}
}