Actegories, Copowers, and Higher-Order Message Passing Semantics
本文通过将右作用范畴与右富集范畴的等价性从封闭对称情形推广至非封闭非对称情形，为支持高阶进程传递的并发语言 CaMPL 提供了必要的语义基础，解决了线性资源无法复用所导致的高阶定义难题。
🧩 Category
cs.PL
27 篇论文
Floating-Point Usage on GitHub: A Large-Scale Study of Statically Typed Languages
本文通过对 GitHub 上数百万静态类型语言仓库的大规模实证研究，揭示了现实世界中浮点数算术的使用特征，验证了现有基准测试的部分代表性并指出了其不足，同时发布了一个包含 1000 万个真实浮点函数的数据集以推动相关自动推理技术的发展。
Turn: A Language for Agentic Computation
本文介绍了 Turn，一种专为代理软件设计的编译型、基于 Actor 的编程语言，它通过认知类型安全、置信度操作符、隔离的 Actor 进程模型、基于能力的身份系统以及编译时模式吸收等五项语言级构造，将大语言模型推理、状态管理和凭证隔离等关键特性从应用层惯例提升为语言级保障。
Arbiter: Detecting Interference in LLM Agent System Prompts
本文提出了名为 Arbiter 的框架，通过结合形式化评估规则与多模型扫描技术，成功检测出 Claude Code、Codex CLI 和 Gemini CLI 等主流 LLM 编码代理系统提示词中的干扰模式，并揭示了提示架构与故障类别的关联性及多模型评估在发现独特漏洞方面的优势。
Idempotent Slices with Applications to Code-Size Reduction
本文正式化了幂等后向切片的概念，提出了一种基于 GSA 形式的有效提取算法，并通过在 LLVM 测试套件中的实验证明，该算法能够识别并合并非连续指令序列，从而实现高达 7.24% 的代码体积缩减。
vLLM Hook v0: A Plug-in for Programming Model Internals on vLLM
本文介绍了 vLLM Hook v0，这是一个开源插件，旨在突破现有 vLLM 对模型内部状态编程的限制，通过被动监控和主动干预两种机制，支持在推理过程中实时检测对抗提示、增强检索增强生成（RAG）以及实施激活导向等高级功能。
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
本文提出了一种结合语法引导合成（SyGuS）与扩展了谓词和函数更新的时序流逻辑（TSL）的新方法，通过从执行轨迹中挖掘数据转换与时序规范，实现了比被动学习基线更鲁棒且样本效率更高的反应式程序合成。
PolyBlocks: A Compiler Infrastructure for AI Chips and Programming Frameworks
本文介绍了 PolyBlocks，这是一个基于 MLIR 的模块化编译器基础设施，通过组合轻量级仿射分析与启发式成本模型自动执行多级分块、融合及算子映射等优化，实现了从高层框架到特定 AI 芯片的高效代码生成，并在 NVIDIA GPU 上的实验表明其性能可媲美甚至超越 Torch Inductor 和 XLA。
From State Changes to Creative Decisions: Documenting and Interpreting Traces Across Creative Domains
该论文针对现有方法在记录创意活动轨迹时缺乏意图与高层级创意决策关联的问题，提出了三种互补方案，分别通过节点式界面管理生成式 AI 状态、构建可视化创作词汇以及将语义历史嵌入交互状态，以更好地捕捉和解读跨领域的创意实践。
EAGLE-Pangu: Accelerator-Safe Tree Speculative Decoding on Ascend NPUs
本文提出了 EAGLE-Pangu 系统，通过将 EAGLE-3 风格的树形推测解码适配至昇腾 NPU 上的盘古模型，利用显式缓存管理、加速器安全的张量化及融合内核验证路径，在确保可复现性的同时显著提升了端到端解码吞吐量。
Towards a Higher-Order Mathematical Operational Semantics
本文通过将 Turi 和 Plotkin 的双代数抽象 GSOS 框架推广至高阶语言，建立了基于点状高阶 GSOS 律的抽象规范理论，从而为 SKI 演算和-演算等系统的组合性证明提供了通用的数学语义框架。
VyZX: Formal Verification of a Graphical Quantum Language
本文介绍了 VyZX，这是一个基于归纳定义的验证库，旨在解决图形化语言（如 ZX 演算）在形式化验证中因归纳结构而丧失图示特性的问题，通过结合范畴论定义、证明助手技术以及集成可视化 IDE，实现了对量子计算图形语言语义和重写规则的有效形式化推理。
Getting Python Types Right with RightTyper
本文提出了 RightTyper，一种通过结合程序实际执行观测、静态分析和自适应采样技术，在仅增加约 27% 运行时开销的情况下，为 Python 代码生成比现有静态、动态及 AI 方法更准确且精确的类型注解的新型混合工具。
Fully Symbolic Analysis of Loop Locality: Using Imaginary Reuse to Infer Real Performance
这篇论文提出了一种全新的完全符号化局部性理论，通过推导局部性多项式来精确预测科学计算内核的缓存性能，在 41 个基准测试中实现了 99.6% 的数据移动预测准确率，且预测过程仅需不到一毫秒。
Category Theory for Programming
这篇讲义以函数式编程的应用为导向，简要介绍了范畴论中的初始代数（用于刻画数据类型和递归函数）和单子（用于处理语言中的副作用）等核心概念，并包含大量习题与解答。
Linear Layouts: Robust Code Generation of Efficient Tensor Computation Using
本文提出了名为“线性布局”的新方法，通过利用上的线性代数将张量布局建模为二进制矩阵，从而实现了通用且高效的布局定义与转换，显著降低了 Triton 编译器后端的工程复杂度并提升了张量计算性能。
Formally Verified Linear-Time Invertible Lexing
本文介绍了 ZipLex，这是一个基于 Stainless 验证器构建的已验证框架，它通过结合新的令牌序列抽象、Huet 拉链及验证过的哈希表等优化技术，实现了兼具线性时间复杂度、最长匹配语义以及词法分析与打印互为逆运算特性的可逆词法分析。
Hybrid Structured Editing: Structures for Tools, Text for Users
该论文提出了“混合结构化编辑”方法，旨在通过为工具开发者提供结构约束保障、同时为用户维持熟悉的文本编辑界面，解决现有扩展机制难以将工具与文本源代码紧密集成及在编辑中追踪程序结构的问题。
Pitfalls in VM Implementation on CHERI: Lessons from Porting CRuby
本文以 CRuby 移植为例，系统梳理并分类了将虚拟机移植到 CHERI 架构时因 C 语言未定义行为假设与 CHERI 严格内存安全模型冲突而引发的各类实现陷阱，并提供了相应的解决方案与验证。
Evaluating LLMs in the Context of a Functional Programming Course: A Comprehensive Study
本文通过构建包含代码生成、修复和解释的三大基准测试，评估了九种先进大语言模型在低资源函数式编程语言 OCaml 教学环境中的表现，发现尽管其解决作业问题的成功率低于在 Python 和 Java 等主流语言上的表现，但在修正语法类型错误及解答基础概念问题上仍具有显著效用，并提出了旨在提升模型能力、引导学生认知局限及推动领域特定推理研究的未来方向。