arXiv 2602.067152026-02-06cs.PL

实用的会话类型推断（扩展版）

Practical Refinement Session Type Inference (Extended Version)

University of Edinburgh（爱丁堡大学）；Boston University（波士顿大学）

Toby Ueno, Ankush Das

阅读 PDF

arXiv 页面 ↗HTML 原文 ↗

AI总结：

本文提出了一种带算术细化的会话类型系统类型推断算法，并通过优化使其在实际应用中可行。

摘要：

会话类型通过在类型中静态捕捉进程之间的交互协议，来表达并强制并发消息传递系统中的安全通信。最近的工作在会话类型中扩展了算术细化，这使得通信能够进行更细致的描述，但给程序员带来了额外的注释负担。为减轻这种负担，我们提出了一种会话类型系统中带有算术细化的类型推断算法。我们开发了会话类型的子类型理论，包括一个算法，该算法被证明在基于类型模拟的语义定义下是正确的。我们还提供了一个形式推断算法，该算法生成类型和算术约束，然后使用Z3 SMT求解器来解决这些约束。该算法已在Rast语言上实现，并包含三个关键优化，使推断变得可行和实用。我们通过在六个具有挑战性的基准上评估我们的推断引擎来评估其有效性，从一元和二元自然数到线性λ-演算。我们展示了我们的优化在使Z3在合理时间内解决算术约束方面提供的性能优势。

英文摘要：

Session types express and enforce safe communication in concurrent message-passing systems by statically capturing the interaction protocols between processes in the type. Recent works extend session types with arithmetic refinements, which enable additional fine-grained description of communication, but impose additional annotation burden on the programmer. To alleviate this burden, we propose a type inference algorithm for a session type system with arithmetic refinements. We develop a theory of subtyping for session types, including an algorithm which we prove sound with respect to a semantic definition based on type simulation. We also provide a formal inference algorithm that generates type and arithmetic constraints, which are then solved using the Z3 SMT solver. The algorithm has been implemented on top of the Rast language, and includes 3 key optimizations that make inference feasible and practical. We evaluate the efficacy of our inference engine by evaluating it on 6 challenging benchmarks, ranging from unary and binary natural numbers to linear $λ$-calculus. We show the performance benefits provided by our optimizations in coercing Z3 into solving the arithmetic constraints in reasonable time.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

AI总结：

摘要：

英文摘要：

相关论文