发表机构
The Hong Kong University of Science and Technology（香港科学与技术大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究针对智能体系统设计ETAS语言，核心方法是通过规范一致性分配类型并用行为索引跟踪计算，主要贡献是为智能体执行相关推理提供编程语言基础，涵盖授权、非确定性等方面，还实现了该语言并形式化相关性质。
AI 中文摘要
ETAS是一种用于智能体系统的编程语言，它将模型支持的智能体、工具调用、提示、类型化内存、人工审批、策略和执行跟踪视为语义程序元素，而非库约定。它将确定性计算与智能体的非确定性和外部可见动作分离，同时保持直接的编程风格。本文介绍了ETAS的核心设计。其静态语义通过规范一致性分配普通类型，并用两个行为索引跟踪每个计算：一个逃逸效果行和它可能请求的类型化动作跟踪的持久抽象。规范形成一个终止的编译时约束演算。动态语义区分请求、处理、拒绝和提交的事件。还形式化了核心演算和状态保存等性质，并在Rust中实现了ETAS。ETAS为智能体执行前和执行期间的授权、非确定性、恢复和审计证据推理提供了编程语言基础。
英文摘要
ETAS is a programming language for agent systems that treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements rather than library conventions. It separates deterministic computation from agentic nondeterminism and externally visible actions while preserving a direct programming style. We present the core design of ETAS. Its static semantics assigns ordinary types through spec conformance and tracks each computation with two behavioral indices: an escaping effect row and a persistent abstraction of the typed action trace it may request. Specs form a terminating compile-time constraint calculus: type specs provide evidence for polymorphism and resource facts, callable specs constrain function and stage shapes, and trace specs express allow, deny, and temporal constraints. Typing checks requested traces against compiled monitors and emits residual obligations when dynamic resources preclude a complete static proof. The dynamic semantics distinguish requested, handled, denied, and committed events; handlers interpret typed actions without making their requests invisible to authorization or audit. We formalize a core calculus and state preservation, progress, type/effect soundness, handler trace-transparency, and policy safety. We also implement ETAS in Rust with a command-line interface, typed HIR checks, effect and policy diagnostics, handler checks, and trace-aware execution hooks. ETAS provides a programming-language foundation for reasoning about authorization, nondeterminism, recovery, and audit evidence before and during agent execution.
