Paper deep dive
ETAS: An Effect-Typed Language for Agent Systems
Huiri Tan, Yikun Wang, Puyang Zhang, Shangyu Li, Jiasi Shen
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 7/21/2026, 5:42:37 AM
Summary
The paper introduces ETAS, an effect-typed programming language designed for agent systems. It treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as first-class semantic program elements. ETAS separates deterministic computation from agentic nondeterminism and externally visible actions, using a static semantics that assigns types through spec conformance and tracks computations with behavioral indices (escaping effect rows and persistent action traces). The language formalizes a core calculus with type/effect soundness, handler trace-transparency, and policy safety, and provides a Rust-based prototype implementation.
Entities (6)
Relation Signals (5)
Huiri Tan → affiliatedwith → The Hong Kong University of Science and Technology
confidence 95% · Huiri Tan The Hong Kong University of Science and Technology
ETAS → implementedin → Rust
confidence 95% · We also implement ETAS in Rust with a command-line interface
ETAS → implements → Effect-Typed Semantics
confidence 95% · ETAS is a programming language for agent systems that treats model-backed agents... as semantic program elements... static semantics assigns ordinary types through spec conformance
ETAS → comparesto → LangGraph
confidence 90% · Figure 1 makes the mismatch concrete by showing the same draft-approve-publish workflow in two representations. The left panel uses the documented shape of LangGraph’s StateGraph API
TraceSpecAlgebra → usedby → ETAS
confidence 85% · trace specs normalize into TraceSpecAlgebra objects over allow, deny, and temporal constraints
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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.
Tags
Links
- Source: https://arxiv.org/abs/2607.17780v1
- Canonical: https://arxiv.org/abs/2607.17780v1
Trouble viewing inline? Open PDF directly →
Full Text
137,898 characters extracted from source content.
Expand or collapse full text
Etas: An Effect-Typed Language for Agent Systems Huiri Tan The Hong Kong University of Science and TechnologyHong KongHong Kong , Yikun Wang The Hong Kong University of Science and TechnologyHong KongHong Kong , Puyang Zhang The Hong Kong University of Science and TechnologyHong KongHong Kong , Shangyu Li The Hong Kong University of Science and TechnologyHong KongHong Kong and Jiasi Shen The Hong Kong University of Science and TechnologyHong KongHong Kong Abstract. Etas is a programming language designed for agent systems. It treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements rather than library conventions. The central idea is to separate deterministic computation from agentic nondeterminism and externally visible actions, while retaining the direct programming style expected by application programmers. This paper presents the core design of Etas. The static semantics assigns ordinary types to values through typing with spec conformance and an active monitor context. A computation is checked 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 normalize into TraceSpecAlgebra objects over allow, deny, and temporal constraints. Typing checks the requested trace against monitors compiled from these trace objects and emits explicit residual obligations when dynamic resources prevent a complete static proof. The dynamic semantics records requested, handled, denied, and committed events, and mediates concrete actions against policies, handlers, deployment permissions, effect boundaries, and the current trace prefix. We formalize a core calculus where source declarations elaborate to checked callable descriptors and handlers mediate typed actions without erasing their traces. We state preservation, progress, type/effect soundness, handler trace-transparency, and policy safety. We implemented an Etas prototype in Rust with a user-facing CLI, typed HIR checks, effect/policy diagnostics, handler checks, and trace-aware execution hooks. The result is a PL foundation for building agent systems whose authorization, nondeterminism, recovery behavior, and audit evidence can be reasoned about before and during execution, even when handlers make some requested effects non-escaping. programming languages, agent systems, effects, policy enforcement, semantics †copyright: none†ccs: Software and its engineering Formal language definitions†ccs: Theory of computation Program semantics 1. Introduction Agent systems are already programs, but they are not yet treated as programs. A production agent application has control flow, state, data dependencies, nondeterministic subcomputations, externally visible effects, resource contracts, failure recovery paths, and audit traces. It branches, calls tools, updates memory, delegates to specialized agents, asks humans for approval, retries failed work, and resumes from checkpoints. Yet the dominant way to build such systems is still framework-level composition: a programmer writes ordinary host-language code around prompt templates, tool registries, vector stores, model providers, guardrails, and logging hooks. Addressing this mismatch is the central motivation for Etas. The logical structure of an agent system is program structure, but it is commonly represented as host-language objects, callbacks, configuration files, and operational logs rather than as source-level syntax with types, effects, and semantics. As a result, questions that should be answered by a programming language are answered by convention. Which actions may a model request? Which memory regions may an agent read or write? Was approval obtained before a high-impact action? Can a run be replayed without repeating an irreversible operation? Does untrusted text flow into a privileged prompt channel? Can a retry duplicate an irreversible side effect? These are not merely framework engineering questions. They are questions about the meaning of a program. A missing programming-language account. Figure 1 makes the mismatch concrete by showing the same draft-approve-publish workflow in two representations. The left panel uses the documented shape of LangGraph’s StateGraph API (LangChain, 2026). Its code structure merely exposes The graph, state schema, and node order without deeper semantic information. The right panel expresses the same workflow as an Etas program, where rich semantic information such as model inference, approval, policy, and email are exposed as source-level facts. ⬇ from typing_extensions import TypedDict from langgraph.graph import StateGraph, START, END class State(TypedDict): topic: str draft: str approved: bool def draft(s: State): return "draft": call_model(s["topic"]) def publish(s: State): if s["approved"]: send_email(s["draft"]) return g = StateGraph(State) g.add_node("draft", draft) g.add_node("publish", publish) g.add_edge(START, "draft") g.add_edge("draft", "publish") g.add_edge("publish", END) app = g.compile() (a) Framework graph. ⬇ @model("reasoner") agent Draft(req: DraftRequest) → Report let prompt = Prompt.new() .system(Trusted("Draft a short update.")) .data(req); return perform infer<Report>(prompt); spec PublishPolicy: trace = +Approval.request & +CompanyEmail.send<WorkAccount> & (Approval.request >> CompanyEmail.send<WorkAccount>); flow publish(req: DraftRequest) → unit ![Approval.request, CompanyEmail.send<WorkAccount>] ~ PublishPolicy let draft = Draft.run(req); if std.ui.approve("send draft", draft, risk = High) perform CompanyEmail.send(WorkAccount, req.to, "Draft update", draft.markdown); (b) Etas program. Figure 1. Draft-approve-publish workflow in framework code and Etas. The framework graph exposes state and callback order but not email authority or approval dominance; Etas makes inference, effects, and PublishPolicy source-level facts for static checking, audit, and replay. Side-by-side code comparison. The left panel shows a LangGraph-style StateGraph with draft and publish callbacks. The right panel shows an Etas program with typed actions, a publish trace spec, and an effect row. The design of Etas enables the static analysis and optimization for agent systems. The example is deliberately small. Static analysis is difficult in the framework version because neither the state schema nor the graph edges say that publish may send email, that approved is an approval token with a particular scope and freshness, or that every path to the email action is dominated by an approval event. A framework can add runtime middleware, interrupts, or guardrails, but the property is not a source-level effect and policy fact. In the Etas version, static analysis is easier because the email authority appears as the action .⟨⟩ CompanyEmail.send WorkAccount , the flow’s effect row exposes possible approval and email actions, and PublishPolicy is a trace spec stating the temporal obligation that approval must precede email. Similarly, optimization is difficult in the framework version, because draft is a nondeterministic model call and publish may perform an irreversible external action, but both are ordinary Python callbacks. In Etas, optimization is easier because Draft.run records the requested action .⟨.,⟩ Agentic.infer Draft.run, Report , and perform CompanyEmail.send gives the compiler and runtime the distinction they need for replay, caching, scheduling, residual policy checks, and deployment manifests, rather than reconstructing those facts from callback code and logs. If agent systems are programs, then the relevant program elements are not only expressions, functions, and modules. They also include flows, agents, model-callable tools, prompt values, typed memory regions, policies, approvals, handlers, runtime resource limits, and traces. A language for agent systems should make these elements explicit enough to check, compile, execute, audit, replay, and optimize them. Table 1. Capability comparison across representative agent frameworks, effect languages, and coordination-oriented programming models. Check marks, triangles, and crosses denote native, partial, and absent support. System Agent constructs Typed communication Effect/action inference Policy automata Approval and limits Prompt trust Semantic trace/replay Runtime enforcement LangGraph / LangChain (LangChain, 2026) △ △ ✗ ✗ △ △ ✓ △ AutoGen (Microsoft, 2026b) △ △ ✗ ✗ △ △ △ △ CrewAI (CrewAI, 2026) △ △ ✗ ✗ △ △ △ △ Eino (CloudWeGo, 2026) △ △ ✗ ✗ △ ✗ △ △ OpenAI Agents SDK (OpenAI, 2026) △ △ ✗ ✗ △ △ △ △ Microsoft Agent Framework (Microsoft, 2026a) △ △ ✗ ✗ △ ✗ △ △ Koka / Links / Frank-style effect languages (Leijen, 2014, 2017; Hillerström and Lindley, 2016; Lindley et al., 2017) ✗ ✗ ✓ ✗ ✗ ✗ ✗ △ Capability/effect systems (Brachthäuser et al., 2022) ✗ ✗ ✓ ✗ ✗ ✗ ✗ △ Choral / choreographic programming (Giallorenzo et al., 2024; Bates et al., 2025) ✗ ✓ ✗ ✗ ✗ ✗ ✗ △ Etas ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ Table 1 summarizes the current gap by capability rather than by implementation mechanism. Contemporary agent frameworks provide orchestration, memory, human-in-the-loop controls, guardrails, tracing, and deployment, but expose them mainly as host-language APIs or platform services (LangChain, 2026; Microsoft, 2026b; CrewAI, 2026; CloudWeGo, 2026; OpenAI, 2026; Microsoft, 2026a). Conversely, effect languages provide a well-founded account of typed effects and handlers (Leijen, 2017; Hillerström and Lindley, 2016; Lindley et al., 2017), but they are not designed around model inference, model-callable tools, approval-dominated side effects, prompt trust, durable traces, or replay. The missing point is a language whose semantic objects are precisely the authority, policy, nondeterminism, and trace boundaries that agent frameworks currently manage outside the type system. Etas is our answer to this missing account. It does not try to make model outputs deterministic, to replace the platforms that host agent workloads, or to present agents, effects, policies, and monitors as separate inventions. The contribution is their combination as one language semantics: agentic nondeterminism, authority-bearing actions, trace safety specs, and typed tool surfaces are checked and executed as parts of the same program. First-class agent structure. In Etas, an agent is not an SDK object hidden behind a class interface. It is a compiler-visible semantic node. An agent declaration has input and output types, a model-inference boundary, a tool surface, prompt and context construction, nondeterminism, trace and replay behavior, and an action summary. A flow that calls an agent is therefore not merely calling a Python callback. It is entering a typed region in which model-backed inference may occur, selected tools may be requested, and trace events may be produced. This is what lets the compiler reason about agent fusion, tool-surface specialization, context-harness optimization, effect-aware scheduling, checkpointing, replay, and audit, rather than rediscovering these facts from framework objects and logs. Action-centric effects. Etas follows typed effect systems and algebraic effects (Plotkin and Power, 2003; Plotkin and Pretnar, 2013; Bauer and Pretnar, 2015; Leijen, 2014, 2017), but it uses effects for the semantics of an agent runtime rather than as unrestricted programmable control. An effect name describes a behavioral family, such as company email or filesystem access. An action is the concrete authority boundary inside that family: sending through a work account and reading a path within a reports root are different parameterized actions. A perform is a traceable, interceptable, auditable runtime event. Handlers may interpret selected action requests for testing, replay, recovery, or host adaptation, but handlers do not grant authority. Authorization remains a property of the active effect boundary, deployment grants, policy, approval evidence, and sandboxing. This distinction matters because handling an action should not erase the fact that the action was requested. A conventional effect handler may explain an operation and thereby remove the corresponding obligation from the caller. That is the right account for control, but it is not enough for safety and audit in agent systems. If a flow attempts to send email and a dry-run handler intercepts the request, no external email is committed; nevertheless, the attempt is still relevant to authorization, replay, and audit. Etas therefore separates the effects that still escape to the caller from the action requests that occurred along the way. A handler may discharge the control obligation for CompanyEmail.send, but the trace still records that the program asked for email authority. Agent-runtime actions such as model inference are treated in the same spirit: they are visible to trace planning, policy, and replay even when they are not exposed as ordinary user-facing effects. Specs as static constraints. Etas uses spec as a uniform compile-time abstraction for constraints over types, callable shapes, and traces. Trace specs are the source-level form of safety policy, but they are only one branch of the same conformance system. Type specs provide trait-like evidence for polymorphic functions and resource relations; callable specs constrain flow, tool, and agent-method shapes; trace specs constrain requested actions. During checking, type specs produce witnesses and callable specs produce callable artifacts in the static signature. Trace specs are kind-checked, normalized to TraceSpecAlgebra objects, compiled to monitors, and used during typing to check the requested-action abstraction. When the compiler can prove that the requested trace satisfies the active monitors, no run-time check is needed. When the answer depends on run-time information such as paths, tenants, approval freshness, or model-chosen tool arguments, the compiler makes that obligation explicit as a residual check. When the monitor is definitely violated, the program is rejected. System consequences. The semantic split above yields system-level capabilities that are hard to obtain when agent behavior is scattered across callbacks, middleware, logs, and deployment configuration. For safety, the compiler can detect missing approvals, forbidden resource access, hidden authority, prompt-trust violations, and tools that expose effects outside their declared surface. For reliability, trace, replay, resampling, checkpointing, and bounded execution are language-level semantics rather than framework conventions. For optimization, the compiler can use agent/action summaries to specialize tool surfaces, fuse compatible agent regions, optimize context construction, and schedule around effects. For auditability, every action request, handler decision, approval, tool call, commit, and denial belongs to the same typed trace vocabulary. For enforcement, static analysis and dynamic monitoring are deliberately connected: static checking is conservative, and every obligation it cannot prove is made explicit as a residual runtime check. Contributions. This paper makes the following contributions. (1) We identify first-class semantic constructs for production agent systems: flows, agents, model-callable tools, typed prompts and messages, scoped memory, approvals, handlers, and traces. These constructs make model inference, tool surfaces, context harnesses, replay, and nondeterminism visible to the compiler. (2) We formalize an action-centric effect system in Core Etas, a small calculus that separates values from computations, deterministic flow calls from agentic inference, escaping effects from persistent requested-action traces, and ordinary tool values from authority-bearing action requests. (3) We give a static semantics based on typing with spec conformance. The type-and-effect system distinguishes effects that escape to callers from typed actions that may be requested even when handlers interpret them. The static signature carries declaration summaries and conformance evidence, while any obligation that cannot be proved statically is made explicit as a residual run-time check. (4) We define spec as a unified compile-time calculus for type, callable, and trace constraints. Type specs provide evidence for trait-like polymorphism, callable specs constrain function and stage polymorphism, and trace specs normalize to TraceSpecAlgebra objects that compile to monitors, where automata and abstract interpretation produce either a static proof, residual checks, or rejection. (5) We give a dynamic semantics in which every concrete action is split into request, handled, denied, and commit events. Request events are policy-visible; commit events require effect-boundary, deployment, approval, and sandbox authorization. We state the corresponding preservation, progress, type-soundness, effect-soundness, handler trace-transparency, and policy-safety theorems. (6) We implement a prototype in Rust: a user-facing compiler and interpreter, typed HIR checking, effect/policy commands, handler diagnostics, package metadata, checkpoint/resume interfaces, interpreter-enforced token and attempt limits, and a test suite of source fixtures. We also evaluate our approach for ensuring the safety, reliability, optimization, audit, and static–dynamic enforcement benefits of the design. Paper structure. Section 2 first develops the language through a running example. Section 3 then defines the core calculus. Section 4 presents types, effects, trace specs, TraceSpecAlgebra, policy automata, and abstract interpretation. Section 5 defines traces and runtime enforcement. Section 6 states the main safety theorems. Section 7 and Section 8 discuss the prototype and evaluation plan, and Section 9 situates the design among effects, handlers, capabilities, runtime monitoring, choreographic languages, and agent-oriented programming models. Section 10 concludes. 2. Overview This section introduces Etas through a small but representative agent workflow. The syntax is intentionally surface-level. The core calculus used for the formal development appears in Section 3. A safe report-writing workflow. Consider an organization that uses an agent to prepare a technical report from a project workspace. The workflow in Figure 2 may search the web, read a typed memory region containing prior reports, ask a model to draft prose, write a file, and send a notification. Two properties are required. First, workspace writes and email sends must be explicitly approved. Second, secret values may be read by deterministic code but must not be placed in a model prompt unless they are declassified. ⬇ type ProjectMemorySchema = MemoryRegion< Reports: Store<ReportId, Report>, Secrets: Store<SecretId, SecretValue<string>>, >; let ProjectMemory = std.memory.region<ProjectMemorySchema>(stable_id = "project_memory", store = "project-main"); tool search_web(q: string) → SearchResults ![Web.search<_>]; tool write_report(path: string, body: string) → unit ![ProjectWorkspace.write<"reports/**">]; tool notify(owner: UserId, path: string) → unit ![CompanyEmail.send<WorkAccount>]; flow DraftPrompt(req: DraftRequest) → Prompt ![Memory.read<ProjectMemory.Reports>] let prior = ProjectMemory.Reports.get(req.related); return Prompt.new() .system(Trusted("Write a concise technical report.")) .data( request = req, prior ); @model("GPT-5.5-Pro") @tools([search_web]) @limits([Tokens(12000), Attempts(2)]) agent DraftReport(req: DraftRequest) → Report ![Memory.read<ProjectMemory.Reports>, Web.search<_>] return perform infer<Report>(DraftPrompt(req)); spec ApprovalBefore<A: Action> = +Approval.request & +A & (Approval.request >> A); spec PublishPolicy = ApprovalBefore<ProjectWorkspace.write<"reports/**">> & ApprovalBefore<CompanyEmail.send<WorkAccount>>; flow publish_report(req: DraftRequest) → ReportPath ![Web.search<_>, Memory.read<ProjectMemory.Reports>, Approval.request, ProjectWorkspace.write<"reports/**">, CompanyEmail.send<WorkAccount>, Error<PolicyDenied>] ~ PublishPolicy let draft = DraftReport.run(req); let path = "reports/" + req.id + ".md"; if !std.ui.approve("Publish report?", draft, risk = High) abort("publish rejected"); write_report(path, draft.markdown); if !std.ui.approve("Notify owner?", req.owner, risk = Medium) abort("notify rejected"); notify(req.owner, path); return path; Figure 2. Surface Etas program for safe report drafting and publication. The example exposes typed memory, tool action rows, model/tool configuration, resource limits, and ApprovalBefore trace specs. The publish_report row bounds escaping actions; dynamic facts such as exact paths or approval freshness remain residual checks. Limits are operational, not part of the Core Etas metatheory. An Etas program that defines a typed project memory region, web search, report writing, email notification, a report-drafting agent, approval trace specs, and a publishing flow with an effect row and requested-action trace constraint. The figure illustrates four separations that are central to the language. First, the agent method is ordinary checked code that constructs a Prompt and reaches model nondeterminism only at ⟨⟩perform\ infer Report ; it does not perform publishing. Second, @tools([search_web]) exposes a model-callable boundary to the agent without granting ambient authority to the surrounding flow. Third, memory access is typed and effectful. The report agent may read prior reports, while values from ProjectMemory.Secrets are SecretValues and are not prompt-encodable unless an explicit declassification flow is used. Fourth, the approvals are ordinary support-flow calls whose effect is visible in the row, while the policy is written as a trace spec that gives them temporal meaning over the requested trace. The @limits annotation additionally gives the interpreter a token-and-attempt contract for model execution. This is an operational language feature rather than part of the Core Etas effect-and-trace metatheory. Effects summarize obligations, traces summarize requests. The type of publish_report contains not only its input and output types, but also a row of effects that may escape to the caller. The row is an upper bound on escaping obligations: a particular execution may not search the web if the model does not invoke the search tool, but any execution that commits a search through the default runtime must do so through the declared action. This matches the practical role of row-typed effects in Koka (Leijen, 2014, 2017), while shifting the domain from exceptions, state, or iterators to authority-bearing agent runtime operations. The public row contains ordinary escaping actions, such as workspace writes under reports/, memory reads, approval requests, and email sends. Separately, the compiler records a requested-action trace abstraction, including metadata such as .⟨.,⟩ Agentic.infer DraftReport.run, Report for the inference operation inside the agent method. This abstraction is consumed by the runtime provider, policy checker, trace system, and replay engine; it is not identical to the set of effects that remain unhandled. The distinction matters because a model call is not a tool call and not a deterministic function call: it is a controlled point of nondeterminism. Trace specs compile to policies. PublishPolicy is a compile-time trace spec, not a runtime callback. The reusable spec function ⟨A⟩ ApprovalBefore A abstracts the common constraint that an approval request is allowed, the target action is allowed, and the approval must precede the target action. Instantiating it for workspace writes and email sends beta-reduces at compile time to a TraceSpecAlgebra normal form containing allow rules and temporal obligations. These obligations are not local type constraints. They require a temporal relation between events: a trace prefix ending in a workspace-write action is permitted only if the prefix already contains a suitable Approval.request event with a matching scope. Etas compiles TraceSpecAlgebra objects to finite monitors over typed action traces. The static checker then interprets the program over an abstract trace domain; if every abstract trace is accepted by the monitor, the trace spec is statically discharged. If a clause depends on dynamic data, such as the exact report path or approval freshness, the compiler emits a residual runtime check. This is only the trace-kind branch of spec. Type specs resolve to evidence for generic functions and resource-indexed actions; callable specs constrain the shape and effect row of flows, tools, generated agent methods, and composed stages. Table 2. Selected static facts inferred for the overview example. Category Property Inferred fact Structure Model boundary records .⟨.,⟩ Agentic.infer DraftReport.run, Report Tool surface exposes web search only through search_web Authority Tool actions may search web, write workspace, send email Memory actions may read ProjectMemory.Reports Requested trace includes model, approval, write, and email requests Policy Approval obligations approval before write and email Secret flow secret-to-model path rejected or residual-checked Runtime Trace plan checkpoint model, tool, approval, and write events Deployment plan manifests required actions and residual checks Resource contract interpreter-enforced token and attempt limits Handled does not mean invisible. Suppose a test wants to replace notify with a mock implementation. Etas supports a scoped handler for the email request. If the handler turns the send into a dry run, the email effect no longer escapes to the caller: :−>![]A∋(.⟨⟩). array[]l DryRunEmail:EmailRequest->EmailResult![]\\ A request( CompanyEmail.send WorkAccount ). array Thus the handler eliminates the caller’s control obligation but not the audit fact that the program requested email. Policy can still inspect that request, and a real commit still requires the active effect boundary, deployment grants, policy, and sandboxing. This restriction intentionally differs from fully general algebraic effects (Plotkin and Pretnar, 2013; Kammar et al., 2013; Lindley et al., 2017). The goal is not to make all control effects programmable. The goal is to let tests, replay, recovery, and host adapters interpret selected runtime actions without undermining the authority model. What the compiler learns. From the example, the compiler can extract the summary shown in Table 2. This summary is useful before execution: it drives diagnostics, deployment manifests, policy checks, scheduling decisions, and trace planning. 3. Core Etas Core Etas is an internal calculus. It is not intended to be the full surface language. Its purpose is to isolate the semantic commitments that make agent programs analyzable: values are separated from effectful computations; agent and tool boundaries are represented by checked descriptors; external authority is represented by performed actions; and every action produces a trace event. 3.1. Syntax Figure 3 gives the selected internal grammar. Primitive p covers unit, booleans, numbers, and strings; values also include records, unary functions, and first-class handlers. Expressions add call-by-value application and binding, checked calls, performed actions, and handler application. A handler packages action arms as a value. Its arm-local resume and finish forms are checked only by the affine arm judgment in Figure 6; we write u when an expression is checked in that mode. x∈p∈c∈a0∈ handler armsr::=a0(x¯)⇒ehandler valuesh::=r¯valuev::=x∣p∣⟨ℓi=vi⟩i∈I∣λx.e∣hexpre::=v∣e1e2∣x=e1e2∣ee1e2∣c(e¯)∣a0(v¯)∣eeh∣e∣e array[]@c@ gatheredx∈ Var p∈ Primitives c∈ CallableName\\ a_0∈ ActionLabel gathered\\[-1.29167pt] 416.27809pt0.35pt\\[-0.86108pt] array[]llclhandler arms&r&::=&a_0( x) e\\[2.84526pt] handler values&h&::=&handler\ \ r\\\[2.84526pt] value&v&::=&x p _i=v_i _i∈ I λ x.e h\\[5.69054pt] expr&e&::=&v e_1\,e_2 \ x=e_1\ in\ e_2\\ && &if\ e\ then\ e_1\ else\ e_2 \ c( e) \ a_0( v)\\ && &handle\ e\ with\ e_h\\ && &resume\ e \ e array array Figure 3. Selected internal syntax of Core Etas. The figure lists metavariables, handler arms and values, ordinary values, and expressions. Named calls enter checked callable boundaries, performed actions request typed authority, and resume/finish are accepted only in handler-arm mode. Grammar for primitive values, checked callable names, action labels, handler values, handler arms, and expressions in Core Etas. Source declarations are not core expressions. Flows, agent methods, tools, and standard-library wrappers elaborate to checked callable descriptors c, with summaries Ξ(c)=τi¯⇒τo!ϵ⊳A (c)= _i _o !ε A and unary implementations obtained through (c) body(c). Named entry calls use c(e¯)call\ c( e), while local higher-order code uses ordinary application; multi-argument functions elaborate by nesting. Specs likewise remain in the declaration layer: type and callable conformance contribute evidence to Ξ , whereas trace specs compile to the monitor context Π . They are never runtime redexes. A core program is therefore an entry expression e0e_0 together with Ξ , Π , and the meta-level body lookup; agent and tool metadata is observed through callable and action signatures rather than additional expression forms. An elaborated action label a0a_0 is an opaque authority name whose static resource arguments have already been resolved. Its signature in Ξ determines argument and result types, the escaping row, and a requested-trace template. We write a=a0(v¯)a=a_0( v) for a concrete instance. Inference, tool use, memory access, approval, and host I/O are standard action signatures rather than additional core productions; for example, ⟨T⟩(p)perform\ infer T (p) becomes .⟨g,T⟩(p)perform\ Agentic.infer g,T (p), where g identifies the enclosing agent method. Finally, for and while are surface derived forms that elaborate to recursive checked callables. Loop-resource accounting is an orthogonal interpreter facility and is not part of Core Etas. The same normalization preserves affine control in handler arms. Other surface composition and handler notations lower compositionally to calls, lets, perform, and eehhandle\ e\ with\ e_h. 3.2. Actions, Effects, and Traces An action is a concrete runtime request. An effect is a static pattern that over-approximates actions that may escape their local handlers. For example, a concrete action may be abstracted by a path-patterned effect: .("/.",v)⪯.⟨"/∗"⟩. ProjectWorkspace.write( "reports/a.md",v) ProjectWorkspace.write "reports/**" . Effects are therefore not permissions by themselves; they are static escaping summaries that must be checked before an action commits through the default runtime dispatcher. Requested-action trace abstractions are separate: they record that an action was requested even when a handler turns it into a mock result, dry run, approval pause, or typed denial. A trace τ∈∗τ ^* is a sequence of concrete events; we write τ⋅ητ·η for appending η. Events distinguish an action request from a handled outcome, an external commit, or a denial, whose phase is j∈,j∈\ request, commit\ and whose cause is ξ∈ξ∈ Denial. Thus a handler may interpret a request without committing its external side effect: the request remains visible to policy and audit, whereas a commit records that the default runtime implementation performed the operation. Figure 11 defines the concrete event domain alongside the rules that produce it. 3.3. Design Restrictions Core Etas imposes three restrictions that distinguish it from general algebraic-effect calculi. (1) Agent inference operations are nondeterministic action points. Calls to an agent method are ordinary checked calls, but each perform infer inside the method cannot be silently duplicated, erased, or reordered unless a trace-equivalence argument justifies the transformation for the relevant request and commit events. (2) Handlers do not grant authority. A handler can interpret an action request and return a value, but it cannot create a commit event for a side effect unless the active effect boundary, policies, deployment grants, and sandbox constraints permit that commit. (3) Tools are authority boundaries for model-callable operations. A tool body may perform actions covered by its summary, but an agent may request only tools explicitly exposed in its descriptor. These restrictions are pragmatic. They sacrifice some expressiveness of general handlers (Plotkin and Pretnar, 2013; Lindley et al., 2017) in exchange for a clearer security and recovery story for agent runtimes. 4. Static Semantics The static semantics has two responsibilities. It assigns ordinary types to values, and it computes conservative summaries of the actions a computation may request. The key difference from a conventional row-typed effect account is that the judgment carries both conformance artifacts and a compiled trace-monitor context. The escaping row records effects that remain obligations for the caller, while a persistent requested-action trace abstraction records actions that the computation may request even if a handler interprets them locally. The conformance artifacts and declaration data are collected in a fixed static signature Ξ , while the monitor environment Π records the trace specs that have been compiled to automata and are active at the current program point. Policy checking is therefore one branch of spec conformance, not a separate verifier after type checking. This design follows the long-standing distinction between values and computations in effect systems (Leijen, 2014, 2017), but changes what the effect judgment remembers for agent-runtime authority and audit. 4.1. Types Figure 4 collects the value types, schemes, contexts, and global signature of the core calculus. X∈Y∈D∈ℓ∈I∈x∈c∈a0∈a∈a♯∈♯S∈κ∈N∈ϵ∈A∈♯χ∈ζ∈ Typesτ::=X∣Dτ¯∣⟨ℓi:τi⟩i∈I∣τ1→τ2!ϵ⊳A∣∃X.⟨τ,(X∼S)⟩∣![ϵh⇒ϵrτ]⊳Ah∣.type schemesσ::=τ∣∀X.σ∣∀X∼S.σscheme instantiationΞ⊢σ↝τ term contextsΓ::=∅∣Γ,x:σstatic signaturesΞ::=⟨Σa,Σc,Σs,Ω⟩action signaturesΣa::=∅∣Σa,a0(x:τi¯)↦⟨τo,ϵ,A⟩callable tableΣc::=∅∣Σc,c↦τi¯⇒τo!ϵc⊳Acspec tableΣs::=∅∣Σs,Y↦S:κevidence tableΩ::=∅∣Ω,χ∼S↦ζ∣Ω,S1⪯S2spec contextsΔ::=∅∣Δ,x:κmonitor contextsΠ::=∅∣Π⊗(N). array[]@c@ gatheredX∈ TyVar Y∈ SpecName D∈ DataCon ∈ Label I∈ FinSet\\ x∈ Var c∈ CallableName a_0∈ ActionLabel a∈ ActionInst a \\ S∈ Spec κ∈ StaticKind N _ alg ε∈ EffRow A \\ χ∈ ConfSubj ζ∈ ConfArt gathered\\[-1.42262pt] 416.27809pt0.35pt\\[-2.84526pt] array[]llclTypes&τ&::=&X D\, τ 1 _i: _i _i∈ I _1→ _2 !ε A\\ && &∃ X.\, τ, Wit(X S) ![ _h _r\ for\ τ] A_h never.\\[2.84526pt] type schemes&σ&::=&τ ∀ X.\,σ ∀ X S.\,σ\\[2.84526pt] scheme instantiation&&& σ _ instτ array\\[-1.42262pt] 416.27809pt0.35pt\\[-2.84526pt] array[]llclterm contexts& &::=& ,x:σ\\[2.84526pt] static signatures& &::=& _a, _c, _s, \\[2.84526pt] action signatures& _a&::=& _a,a_0( x: _i) _o,ε,A \\[2.84526pt] callable table& _c&::=& _c,c _i _o ! _c A_c\\[2.84526pt] spec table& _s&::=& _s,Y S:κ\\[2.84526pt] evidence table& &::=& ,χ S ζ ,S_1 S_2\\[2.84526pt] spec contexts& &::=& ,x:κ\\[2.84526pt] monitor contexts& &::=& compile(N). array array Figure 4. Static ingredients of Core Etas: metavariables, value and handler types, schemes, and typing environments. Function types carry latent escaping effects and requested traces; handler types record handled effects, arm effects, answer type, and arm trace. Ξ , Γ , Δ , and Π hold signatures, terms, spec parameters, and active monitors. Core static domains, value and handler types, polymorphic and constrained type schemes, and the typing environments used by the static semantics. Typing is bidirectional: synthesis infers the value type, whereas checking consumes an expected type. Ξ;Γ;Π⊢e⇒τ!ϵ⊳A⊣RΞ;Γ;Π⊢e⇐τ!ϵ⊳A⊣R ; ; e τ !ε A R ; ; e τ !ε A R Both judgments are indexed by the global signature Ξ , term context Γ , and active monitors Π , and return an escaping row ϵε, requested-action abstraction A, and residual checks R. The signature stores declarations and type/callable conformance artifacts; trace conformance instead extends Π . Core functions are unary and carry ϵε and A; source arity elaborates to nesting, whereas checked boundaries retain signatures τi¯⇒τo!ϵ⊳A _i _o !ε A in Ξ . Records and data constructors provide the remaining value structure. Prompt, trust, memory, and result notions are prelude types or specs, not additional core type forms. Constrained schemes ∀X∼S.σ∀ X S.\,σ instantiate only with conformance artifacts from Ξ . In Figure 5, calls and actions resolve signatures in Ξ , accumulate escaping rows, and discharge requested traces against Π . T-Action instantiates the selected Σa _a entry with its arguments. The same rule handles .⟨g,O⟩ Agentic.infer g,O because its signature includes (g) tools(g). A first-class handler has type ![ϵh⇒ϵrτr]⊳Ah ![ _h _r\ for\ _r] A_h, recording handled and produced effects, its answer type, and arm trace. Rule T-HandleWith supplies the contextual answer type and may remove ϵh _h, while ϵh(A) handle_ _h(A) preserves requests and adds handled outcomes. Standalone resume-only handlers are answer-polymorphic; any finish fixes the answer type. Formally, ui¯ gen_ u_i: ui¯(![ϵh⇒ϵrτr]⊳Ah)=∀X.![ϵh⇒ϵrX]⊳Ahif (ui¯) and X is fresh,![ϵh⇒ϵrτr]⊳Ahotherwise. gen_ u_i( ![ _h _r\ for\ _r] A_h)= cases∀ X.\, ![ _h _r\ for\ X] A_h&if nofinish( u_i) and X is fresh,\\ ![ _h _r\ for\ _r] A_h&otherwise. cases Monitor discharge Ξ;Π⊢A↝R ; A R proves an abstract trace, rejects it, or returns checks for runtime-only facts. T-TraceConform compiles trace specs into Π ; type and callable specs use the conformance rules of Figure 9. Handler arms reuse ordinary expression typing with terminal resume and finish; the index υ∈0,1 ∈\0,1\ enforces at most one resume per path. Loops and their affine validation elaborate before the core judgment. T-Var x:∈σΓΞ⊢↝instστ Ξ;Γ;Π⊢⇒x⊳!τ∅⊣∅ T-Val data(v)Γ⊢v:τ Ξ;Γ;Π⊢⇒v⊳!τ∅⊣∅ T-Check Ξ;Γ;Π⊢⇒e⊳!τ′ϵA⊣≡Rτ′τ Ξ;Γ;Π⊢⇐e⊳!τϵA⊣R T-Abs Ξ;Γ,x:τ1;∅⊢⇐e⊳!τ2ϵA⊣∅ Ξ;Γ;Π⊢λx.e⇐τ1→τ2!ϵ⊳A!∅⊳∅⊣∅ T-Call Ξ(c)=¯τi⇒⊳!τoϵcAc ∀i.Ξ;Γ;Π⊢ei⇐τi!ϵi⊳Ai⊣Ri ⊢Ξ;Π↝AcRc Ξ;Γ;Π⊢⇒callc(¯ei)⊳⊔!τo(⨆iϵi)ϵc;A1⋯AnAc⊣∪(⋃iRi)Rc T-Action Ξ(a0(¯:xiτi))=⟨τa,ϵa,A0⟩∀i.Γ⊢vi:τi ⊢=AaA0[¯/vixi]Ξ;Π↝AaRa Ξ;Γ;Π⊢⇒performa0(¯vi)⊳!τaϵaAa⊣Ra T-App Ξ;Γ;Π⊢⇒ef⊳!(→τ1⊳!τ2ϵf′Af′)ϵfAf⊣Rf Ξ;Γ;Π⊢⇐e⊳!τ1ϵeAe⊣Re ⊢Ξ;Π↝Af′Rf′ Ξ;Γ;Π⊢⇒efe⊳⊔!τ2ϵfϵeϵf′;AfAeAf′⊣∪RfReRf′ T-Let Ξ;Γ;Π⊢⇒e1⊳!τ1ϵ1A1⊣R1Ξ;Γ,x:τ1;Π⊢⇒e2⊳!τ2ϵ2A2⊣R2 Ξ;Γ;Π⊢letx=e1ine2⇒⊳⊔!τ2ϵ1ϵ2;A1A2⊣∪R1R2 T-LetHandler Ξ;Γ;Π⊢⇒h⊳!σϵ1A1⊣R1Ξ;Γ,x:σ;Π⊢⇒e2⊳!τ2ϵ2A2⊣R2 Ξ;Γ;Π⊢letx=hine2⇒⊳⊔!τ2ϵ1ϵ2;A1A2⊣∪R1R2 T-If Ξ;Γ;Π⊢⇐e⊳!boolϵ0A0⊣R0Ξ;Γ;Π⊢⇒e1⊳!τϵ1A1⊣R1Ξ;Γ;Π⊢⇒e2⊳!τϵ2A2⊣R2 Ξ;Γ;Π⊢⇒ifethene1elsee2⊳⊔!τϵ0ϵ1ϵ2;A0(⊔A1A2)⊣∪R0R1R2 T-TraceConform Ξ;Δ⊢SΞ⊢∈S⇓trNTalg=ΠScompileΞ(N) Ξ;Γ;⊗ΠS⊢⇒e⊳!τϵA⊣R Ξ;Γ;Π⊢e∼S⇒⊳!τϵA⊣R gathered array[]@l@ T-Var\\[-1.05487pt] 3.30554pt $ $ 44.01831pt $ x:σ∈ 16.38895pt σ _ instτ$ 41.75723pt $ ; ; x τ ! $$ $ array 16.38895pt array[]@l@ T-Val\\[-1.05487pt] 3.30554pt $ $ 34.3631pt $ data(v) 16.38895pt v:τ$ 41.61546pt $ ; ; v τ ! $$ $ array 16.38895pt array[]@l@ T-Check\\[-1.05487pt] 3.1111pt $ $ 60.90668pt $ ; ; e τ !ε A R 16.38895ptτ ≡τ$ 42.94458pt $ ; ; e τ !ε A R$$ $ array\\[2.84526pt] array[]@l@ T-Abs\\[-1.05487pt] 3.30554pt $ $ 52.83386pt $ ; ,x: _1; e _2 !ε A $ 64.70235pt $ ; ; λ x.e _1→ _2 !ε A ! $$ $ array\\[2.84526pt] array[]@l@ T-Call\\[-1.05487pt] 6.33893pt $ $ 130.31711pt $ (c)= _i _o ! _c A_c$ 15.94449pt $ ∀ i.\ ; ; e_i _i ! _i A_i R_i$ 15.94449pt $ ; A_c R_c$ 105.45018pt $ ; ; \ c( e_i) _o !( _i _i) _c A_1 ;·s ;A_n ;A_c ( _iR_i)∪ R_c$$ $ array\\[2.84526pt] array[]@l@ T-Action\\[-1.05487pt] 3.71388pt $ $ 129.95065pt $ (a_0( x_i: _i))= _a, _a,A_0 16.38895pt∀ i.\ v_i: _i$ 15.94449pt $ A_a=A_0[ v_i/x_i] 16.38895pt ; A_a R_a$ 72.20111pt $ ; ; \ a_0( v_i) _a ! _a A_a R_a$$ $ array\\[2.84526pt] array[]@l@ T-App\\[-1.05487pt] 4.0964pt $ $ 161.0807pt $ ; ; e_f ( _1→ _2 ! _f A_f ) ! _f A_f R_f$ 15.94449pt $ ; ; e _1 ! _e A_e R_e$ 15.94449pt $ ; A_f R_f $ 94.03038pt $ ; ; e_f\,e _2 ! _f _e _f A_f ;A_e ;A_f R_f∪ R_e∪ R_f $$ $ array\\[2.84526pt] array[]@l@ T-Let\\[-1.05487pt] 3.1111pt $ $ 114.70311pt $ ; ; e_1 _1 ! _1 A_1 R_1 16.38895pt ; ,x: _1; e_2 _2 ! _2 A_2 R_2$ 93.38484pt $ ; ; \ x=e_1\ in\ e_2 _2 ! _1 _2 A_1 ;A_2 R_1∪ R_2$$ $ array\\[2.84526pt] array[]@l@ T-LetHandler\\[-1.05487pt] 3.1111pt $ $ 112.77525pt $ ; ; h σ ! _1 A_1 R_1 16.38895pt ; ,x:σ; e_2 _2 ! _2 A_2 R_2$ 92.35365pt $ ; ; \ x=h\ in\ e_2 _2 ! _1 _2 A_1 ;A_2 R_1∪ R_2$$ $ array\\[2.84526pt] array[]@l@ T-If\\[-1.05487pt] 3.5pt $ $ 161.52408pt $ ; ; e ! _0 A_0 R_0 16.38895pt ; ; e_1 τ ! _1 A_1 R_1 16.38895pt ; ; e_2 τ ! _2 A_2 R_2$ 127.30278pt $ ; ; \ e\ then\ e_1\ else\ e_2 τ ! _0 _1 _2 A_0 ;(A_1 A_2) R_0∪ R_1∪ R_2$$ $ array\\[2.84526pt] array[]@l@ T-TraceConform\\[-1.05487pt] 3.1111pt $ $ 147.56082pt $ ; S 16.38895pt S _ trN _ alg 16.38895pt _S= compile_ (N)$ 15.94449pt $ ; ; _S e τ !ε A R$ 50.93063pt $ ; ; e S τ !ε A R$$ $ array gathered Figure 5. Core bidirectional typing with spec conformance. Each derivation returns a value type, escaping effects, requested-action abstraction, and residual checks. Calls and applications sequence latent summaries; actions instantiate signatures and discharge requests; conditionals join traces; trace conformance extends the monitor context. The split between ϵε and A preserves handled requests. Boxed labels name rules. Bidirectional typing rules for variables, values, functions, application, let, conditionals, checked calls, performed actions, and trace-spec constraints. T-HandleWith Ξ;Γ;Π⊢⇒e⊳!τϵA⊣R Ξ;Γ;Π⊢⇐eh⊳![⇒ϵhϵrforτ]!AhϵgAg⊣Rg ⊢⊆ϵhϵ=Ab⊔handleϵh(A)AhΞ;Π↝AbRb Ξ;Γ;Π⊢⇒handleewitheh⊳⊔!τϵg(-ϵh)ϵr;AgAb⊣∪RgRRb T-Handler =ansΞ,Γ,Π(¯ui)τr ∀i.=Ξ(ai0(¯:xiτi))⟨τir,ϵi,Ai0⟩ ∀i.Ξ;Γ,¯:xiτi;Π⊢ui⇐τir⇒τr!ϵi′⊳Ai⊣Ri;υi ∀i.≤υi1 =ϵhϵii=ϵr⨆iϵi′=Ah⨆iAi =σgen¯ui(⊳![⇒ϵhϵrforτr]Ah) Ξ;Γ;Π⊢⇒handler⇒ai0(¯xi)ui∈iI⊳!σ∅⊣⋃iRi T-HandlerCheck Ξ;Γ;Π⊢⇒h⊳!σϵA⊣R ⊢Ξ↝instσ⊳![⇒ϵhϵrforτr]Ah Ξ;Γ;Π⊢⇐h⊳![⇒ϵhϵrforτr]!AhϵA⊣R T-Resume ≠τanever Ξ;Γ;Π⊢⇐e⊳!τaϵA⊣R Ξ;Γ;Π⊢resumee⇐τa⇒⊳!τrϵA⊣R;1 T-Finish Ξ;Γ;Π⊢⇐e⊳!τrϵA⊣R Ξ;Γ;Π⊢finishe⇐τa⇒⊳!τrϵA⊣R;0 T-ArmNever Ξ;Γ;Π⊢⇐e⊳!neverϵA⊣R Ξ;Γ;Π⊢e⇐τa⇒⊳!τrϵA⊣R;0 T-ArmLet Ξ;Γ;Π⊢⇒e1⊳!τxϵ1A1⊣R1Ξ;Γ,x:τx;Π⊢u⇐τa⇒⊳!τrϵ2A2⊣R2;υ Ξ;Γ;Π⊢letx=e1inu⇐τa⇒⊳⊔!τrϵ1ϵ2;A1A2⊣∪R1R2;υ T-ArmIf Ξ;Γ;Π⊢⇐e⊳!boolϵ0A0⊣R0 Ξ;Γ;Π⊢u1⇐τa⇒⊳!τrϵ1A1⊣R1;υ1 Ξ;Γ;Π⊢u2⇐τa⇒⊳!τrϵ2A2⊣R2;υ2 =υ⊔υ1υ2 Ξ;Γ;Π⊢ifethenu1elseu2⇐τa⇒⊳⊔!τrϵ0ϵ1ϵ2;A0(⊔A1A2)⊣∪R0R1R2;υ gathered array[]@l@ T-HandleWith\\[-1.05487pt] 3.60138pt $ $ 129.04987pt $ ; ; e τ !ε A R$ 15.94449pt $ ; ; e_h ![ _h _r\ for\ τ] A_h ! _g A_g R_g$ $ _h ε 16.38895ptA_b= handle_ _h(A) A_h 16.38895pt ; A_b R_b$ 118.9709pt $ ; ; \ e\ with\ e_h τ ! _g (ε- _h) _r A_g ;A_b R_g∪ R∪ R_b$$ $ array\\[2.84526pt] array[]@l@ T-Handler\\[-1.05487pt] 6.83783pt $ $ 157.61847pt $ ans_ , , ( u_i)= _r$ 15.94449pt $ ∀ i.\ (a_i^0( x_i: _i))= _i^r, _i,A_i^0 $ 15.94449pt $ ∀ i.\ ; , x_i: _i; u_i _i^r _r ! _i A_i R_i; _i$ $ ∀ i.\ _i≤ 1$ 15.94449pt $ _h=\ _i\_i 16.38895pt _r= _i _i 16.38895ptA_h= _iA_i$ 15.94449pt $ σ= gen_ u_i( ![ _h _r\ for\ _r] A_h)$ 87.48338pt $ ; ; handler\ \a_i^0( x_i) u_i\_i∈ I σ ! _iR_i$$ $ array\\[2.84526pt] array[]@l@ T-HandlerCheck\\[-1.05487pt] 3.5pt $ $ 106.09814pt $ ; ; h σ !ε A R$ 15.94449pt $ σ _ inst ![ _h _r\ for\ _r] A_h$ 76.03377pt $ ; ; h ![ _h _r\ for\ _r] A_h !ε A R$$ $ array\\[2.84526pt] array[]@l@ T-Resume\\[-1.05487pt] 3.1111pt $ $ 66.20503pt $ _a≠ never$ 15.94449pt $ ; ; e _a !ε A R$ 71.66214pt $ ; ; \ e _a _r !ε A R;1$$ $ array 16.38895pt array[]@l@ T-Finish\\[-1.05487pt] 3.1111pt $ $ 44.36798pt $ ; ; e _r !ε A R$ 68.33852pt $ ; ; \ e _a _r !ε A R;0$$ $ array\\[2.84526pt] array[]@l@ T-ArmNever\\[-1.05487pt] 3.1111pt $ $ 47.72258pt $ ; ; e never !ε A R$ 56.6397pt $ ; ; e _a _r !ε A R;0$$ $ array 16.38895pt array[]@l@ T-ArmLet\\[-1.05487pt] 3.1111pt $ $ 127.59515pt $ ; ; e_1 _x ! _1 A_1 R_1 16.38895pt ; ,x: _x; u _a _r ! _2 A_2 R_2; $ 105.9264pt $ ; ; \ x=e_1\ in\ u _a _r ! _1 _2 A_1 ;A_2 R_1∪ R_2; $$ $ array\\[2.84526pt] array[]@l@ T-ArmIf\\[-1.05487pt] 3.5pt $ $ 159.38335pt $ ; ; e ! _0 A_0 R_0$ $ ; ; u_1 _a _r ! _1 A_1 R_1; _1$ 15.94449pt $ ; ; u_2 _a _r ! _2 A_2 R_2; _2$ 15.94449pt $ = _1 _2$ 142.15407pt $ ; ; \ e\ then\ u_1\ else\ u_2 _a _r ! _0 _1 _2 A_0 ;(A_1 A_2) R_0∪ R_1∪ R_2; $$ $ array gathered Figure 6. Typing first-class handlers and handle-with expressions. T-HandleWith removes handled effects from the escaping row while preserving requests in A; T-Handler checks arms against a common answer type and synthesizes reusable schemes. Resume-only handlers remain answer-polymorphic, and arm control permits at most one resume per path. Rules for handle-with expressions, synthesizing and instantiating handler values, resume, finish, non-returning arms, and structured branching in handler arms. 4.2. Effects An effect row ϵε is a finite set of action patterns, with row variables during inference. Surface syntax may use namespace notation, but the core treats rows extensionally: action patternsπ::=μ⟨τ¯⟩effect rowsϵ::=∅∣π∣ϵ∪ϵ. array[]llclaction patterns&π&::=&μ τ \\ effect rows&ε&::=& π ε∪ε. array Here μ is a core action name and τ is a static type argument. Resource regions, accounts, and other selectors are nominal marker types constrained by type specs; containment is derived from their evidence. For example, .⟨⟩⊇.⟨.⟩, Memory.read ProjectMemory Memory.read ProjectMemory.Reports , but not conversely. Read authority also does not imply write authority. trace abstractionsA::=∅∣η♯∣A1;A2∣A1⊔A2∣A⋆abstract eventsη♯::=(a♯)∣(a♯,h)∣(a♯)∣(j(a♯),ξ)residual obligationsR::=∅∣(η♯,φ)∣R1∪R2. array[]llcltrace abstractions&A&::=& η A_1 ;A_2 A_1 A_2 A \\[2.84526pt] abstract events&η &::=& request(a ) handled(a ,h) commit(a ) denied(j(a ),ξ)\\[2.84526pt] residual obligations&R&::=& check(η , ) R_1∪ R_2. array Figure 7. Static requested-action traces and residual obligations. Trace abstractions sequence, join, and iterate abstract request, handled, commit, and denial events. Monitor discharge returns R for dynamic predicates that remain runtime checks, so handled actions stay visible even without escaping effects or commits. The static trace language used by typing rules to summarize request, handled, commit, and denial events, together with residual runtime checks that remain after monitor discharge. Escaping effects and requested actions. Etas tracks two behavioral summaries: Ξ;Γ;Π⊢e⇒τ!ϵ⊳A⊣R. ; ; e τ !ε A R. The escaping effect row ϵε is the public type-level upper bound in flow and tool types: it records effects that remain for the caller to handle or mediate. The requested-action trace abstraction A records which typed actions the computation may request, and in which abstract order, regardless of whether each request is handled, denied, or committed. The monitor environment Π constrains A during typing, and R records residual checks for facts that cannot be discharged statically. Trace specs and runtime audit therefore use A, not just ϵε. The distinction is needed for agent inference and handlers. A public flow type need not expose provider-internal details, but the runtime still needs trace evidence for .⟨g,O⟩ Agentic.infer g,O , model-selected tools, schema validation, and related events. A dry-run email handler may make the effect non-escaping while leaving its typed request auditable. Handling removes a caller obligation; it does not remove trace evidence. Declared rows. For a declaration e:τ!ϵde:τ! _d, the checker requires the inferred row ϵi _i to be covered by the declared row: ϵi⊑ϵd. _i _d. Rows are upper bounds. A missing effect is an error; an unused declared effect is usually a warning unless strict mode requires minimal rows. Declared rows are not complete behavior summaries. They constrain what may escape, while the typing judgment checks the inferred AiA_i against monitors from active trace specs and returns residual obligations. Thus a declaration can honestly say :−>![] DryRunEmail:EmailRequest->EmailResult![] while the compiler still records the possible email request and checks it against the active trace specs. 4.3. Spec Conformance Etas specs are kinded compile-time constraints consumed by the ∼ conformance relation. A type spec constrains types, including resource-marker types; a callable spec constrains callable shape and optional effect bounds, and a trace spec constrains requested actions. The first two produce static artifacts in Ξ ; trace specs compile to monitors in Π . Figure 8 gives the terminating spec calculus. Its single kind grammar κ classifies conformance specs, effect and action parameters, and higher-order spec functions; complete conformance specs have result kind type, callable, or trace. Lambda abstraction and application make specs reusable; for example, ⟨P:⟩ ApprovalBefore P: Action elaborates to λP.+.&+P&(.≫P).λ P action.\,+ Approval.request \&+P \&( Approval.request P). Applications beta-reduce during compilation; recursive and runtime-produced specs are outside the calculus. P∈μ∈static kindsκ::=∣∣∣κ1⇒κ2action patternsp,q::=P∣μ⟨τ¯⟩∣μ⟨X∼S¯⟩callable shapesC::=τi¯⇒τo∣τi¯⇒τo!ϵconformance forms(χ,ζ)::=(τ,w)∣(c,θ)∣(A,R)spec termsS,T::=Y∣xκ∣λxκ.S∣ST∣S1&S2∣S1|S2∣+p∣−p∣p≫q∣p≪q∣(C) array[]llcl @intercol P∈ PatVar 16.38895ptμ∈ ActionName @intercol\\[2.84526pt] static kinds&κ&::=& type callable trace\\ && & effect action _1 _2\\[2.84526pt] action patterns&p,q&::=&P μ τ μ X S \\[2.84526pt] callable shapes&C&::=& _i _o _i _o !ε\\[2.84526pt] conformance forms&(χ,ζ)&::=&(τ,w) (c,θ) (A,R)\\[2.84526pt] spec terms&S,T&::=&Y x^κ λ x^κ.\,S S\,T\\ && &S_1 \&S_2 S_1 |S_2 +p -p\\ && &p q p q callable(C) array Ξ;Δ⊢S:κΞ;Δ⊢p:Ξ⊢S⇓N∈Ξ⊢S⇓C(λxκ.S)T⟶S[x↦T]Ξ(Y)=S:κ⟹Y⟶Sp≪q⟶q≫p array[]c ; S:κ 16.38895pt ; p: action 16.38895pt S _ trN _ alg 16.38895pt S _ callC\\[5.69054pt] (λ x^κ.\,S)\ T S[x T] 16.38895pt (Y)=S:κ Y S\\[2.84526pt] p q q p array Figure 8. Terminating compile-time spec calculus. The figure defines kinds, action patterns, callable shapes, conformance result forms, and spec terms, then gives kinding and normalization. Type, callable, and trace specs produce witnesses, callable artifacts, and residual checks. Applications beta-reduce, named specs unfold, p≪qp q normalizes to q≫pq p, and recursion/runtime specs are excluded. Static kinds, type-indexed action patterns, callable shapes, conformance forms, spec expressions, and normalization judgments for callable and trace specs. Figure 8 also pairs each conformance subject with its artifact: types produce witnesses (τ,w)(τ,w), callables produce static artifacts (c,θ)(c,θ), and requested-trace abstractions produce residual checks (A,R)(A,R). We write the three forms uniformly as χ∼S↝ζχ S ζ; Figure 9 gives their kind-directed rules. The rules are kind-directed. Type conformance resolves witnesses used by constrained schemes ∀X∼S.σ∀ X S.\,σ, without treating conformance as subtyping. Callable conformance normalizes S to an input/output shape and, when present, checks the upper bound ϵc⊑ϵs _c _s; omitting the row leaves it open, whereas ![]![] requires no escaping effects. Trace conformance normalizes S, compiles the result, and discharges A under the extended monitor context, returning R. C-Entail reuses an artifact at a weaker spec. Evidence-indexed action matching reuses the same type-spec witnesses: a bounded argument X∼SX S matches τ exactly when Ξ⊢τ∼S↝w τ S w for some w. C-Type =Ξ(∼τS)w ⊢Ξτ∼S↝w C-Entail ⊢Ξχ∼S1↝ζ ⊢Ξ⪯S1S2 ⊢Ξχ∼S2↝ζ C-Callable Ξ(c)=¯τi⇒⊳!τoϵcAc ⊢Ξ⇓callS(⇒¯τi!τoϵs) ⊑ϵcϵs ⊢Ξc∼S↝θ C-CallableOpen Ξ(c)=¯τi⇒⊳!τoϵcAc ⊢Ξ⇓callS(⇒¯τiτo) ⊢Ξc∼S↝θ C-Trace ⊢ΞS⇓trN∈Talg ⊢Ξ;⊗ΠcompileΞ(N)↝AR ⊢Ξ;ΠA∼S↝R gathered array[]@l@ C-Type\\[-1.05487pt] 2.43054pt $ $ 23.86458pt $ (τ S)=w$ 26.3499pt $ τ S w$$ $ array 16.38895pt array[]@l@ C-Entail\\[-1.05487pt] 3.1111pt $ $ 53.9849pt $ χ S_1 ζ$ 15.94449pt $ S_1 S_2$ 26.20473pt $ χ S_2 ζ$$ $ array\\[2.84526pt] array[]@l@ C-Callable\\[-1.05487pt] 2.43054pt $ $ 95.82085pt $ (c)= _i _o ! _c A_c$ 15.94449pt $ S _ call( _i _o ! _s)$ 15.94449pt $ _c _s$ 25.21065pt $ c S θ$$ $ array 16.38895pt array[]@l@ C-CallableOpen\\[-1.05487pt] 2.43054pt $ $ 73.37779pt $ (c)= _i _o ! _c A_c$ 15.94449pt $ S _ call( _i _o)$ 25.21065pt $ c S θ$$ $ array\\[2.84526pt] array[]@l@ C-Trace\\[-1.05487pt] 3.1111pt $ $ 84.94716pt $ S _ trN _ alg$ 15.94449pt $ ; compile_ (N) A R$ 32.30399pt $ ; A S R$$ $ array gathered Figure 9. Kind-directed conformance from normalized specs to static checking. Type specs resolve witnesses, callable specs check callable shape and optional effect bounds, and trace specs compile to monitors for requested-action abstractions. The resulting artifacts are w, θ, or residual checks R. Conformance rules for type, callable, and trace specs, including entailment and conformance artifacts. For trace specs, Ξ⊢S⇓N S _ trN expands named specs, beta-reduces applications, and computes the TraceSpecAlgebra normal form N. The partial meaning function ⟦⋅⟧N · in Figure 10 maps a closed, well-kinded trace spec to either an atom ⟨L,D,B⟩ L,D,B , containing allow patterns, deny patterns, and before-obligations, or a disjunction of such atoms. normal formsN::=⟨L,D,B⟩∣N1⊕N2allow/deny setsL,D⊆before obligationsB⊆× array[]llclnormal forms&N&::=& L,D,B N_1 N_2\\ allow/deny sets&L,D& & ActionPattern\\ before obligations&B& & ActionPattern× ActionPattern array ⟦⋅⟧:⇀ array[]rclN · &:& TraceSpec _ alg array ⟦+p⟧=⟨p,∅,∅⟩⟦−p⟧=⟨∅,p,∅⟩⟦p≫q⟧=⟨∅,∅,(p,q)⟩⟦S&T⟧=⟦S⟧⊗⟦T⟧⟦S|T⟧=⟦S⟧⊕⟦T⟧⟦(λxκ.S)T⟧=⟦S[x↦T]⟧ array[]rclcrclN +p &=& \p\, , & &N -p &=& ,\p\, \\ N p q &=& , ,\(p,q)\ &&N S \&T &=&N S T \\ N S |T &=&N S T &&N (λ x^κ.\,S)\ T &=&N S[x T] array ⟨L1,D1,B1⟩⊗⟨L2,D2,B2⟩=⟨L1∪L2,D1∪D2,B1∪B2⟩(N1⊕N2)⊗N=(N1⊗N)⊕(N2⊗N)N⊗(N1⊕N2)=(N⊗N1)⊕(N⊗N2). array[]rcl L_1,D_1,B_1 L_2,D_2,B_2 &=& L_1∪ L_2,\ D_1∪ D_2,\ B_1∪ B_2 \\ (N_1 N_2) N&=&(N_1 N) (N_2 N)\\ N (N_1 N_2)&=&(N N_1) (N N_2). array ⟨L,D,B⟩(a)=∃p∈D.Ξ(p,a)∃p∈L.Ξ(p,a)otherwiseτ⊧p≫q⇔∀i.Ξ(q,τi)⇒∃j<i.Ξ(p,τj).τ⊧N1⊗N2⇔τ⊧N1∧τ⊧N2τ⊧N1⊕N2⇔τ⊧N1∨τ⊧N2. array[]rcl decision_ L,D,B (a)&=& cases deny&∃ p∈ D.\ match_ (p,a)\\ allow&∃ p∈ L.\ match_ (p,a)\\ deny&otherwise cases\\[11.38109pt] τ p q& &∀ i.\ match_ (q, _i) ∃ j<i.\ match_ (p, _j).\\[11.38109pt] τ N_1 N_2& &τ N_1 τ N_2\\[11.38109pt] τ N_1 N_2& &τ N_1 τ N_2. array Figure 10. TraceSpecAlgebra normal forms and meaning. Atoms collect allow patterns, deny patterns, and before obligations; ⊕ represents disjunction. Normalization, composition, action decisions, and trace satisfaction appear below the divider. Deny rules take precedence, unmatched actions are denied, and p≫qp q requires prior matching p events. The algebraic normal form for trace specs, the normalization meaning function from trace specs to normal forms, conjunctive composition, evidence-indexed allow-deny resolution, and temporal satisfaction. Deny takes precedence, unmatched actions are denied, and every event matching the target of p≫qp q must have an earlier matching p. The dual p≪qp q normalizes to q≫pq p. Matching is indexed by Ξ , so bounded generic action patterns can reuse ordinary type-spec witnesses. This common conformance boundary is what makes spec more than a policy DSL: it controls type and callable polymorphism as well as typed action traces. 4.4. Policy Automata and Abstract Interpretation Each trace-spec normal form N compiles to a finite monitor MN=⟨Q,q0,δ,⟩M_N= Q,q_0,δ, Bad , where q0q_0 is initial, δ:Q×→Qδ:Q×Ev→ Q, and ⊆Q Bad Q contains rejecting states. Because events distinguish requests, handling, denials, and commits, a request can be constrained independently of its interpretation or commit. The active environment Π denotes their product MΠM_ ; any rejecting component rejects the product, so adding a trace spec only narrows accepted traces. The checker discharges an abstract requested trace with the judgment Ξ;Π⊢A↝R ; A R, defined by abstract interpretation of A over the states of MΠM_ (Cousot and Cousot, 1977). The monitor-state abstract domain is Π♯=(QΠ)D_ =P(Q_ ), and abstract events range over ♯Ev . Its concretization γΞ:♯→() _ :Ev (Ev) uses type-spec evidence from Ξ . For Q♯∈Π♯Q _ , the abstract event transformer is ⟦η♯⟧Ξ,Π♯(Q♯)=δΠ(q,η)∣q∈Q♯,η∈γΞ(η♯). η _ , (Q )=\ _ (q,η) q∈ Q ,\ η∈ _ (η )\. The trace transformer ⟦A⟧Ξ,Π♯ A _ , lifts this definition structurally: sequencing composes transformers, joins union successor states, and A⋆A computes a least fixed point over Π♯D_ ; named boundaries reuse summaries from Ξ . For a successor set Q′Q , Q′∩Π=∅Q ∩ Bad_ = proves the transition safe, while Q′⊆ΠQ Bad_ leaves the judgment without a derivation. In the remaining case, the checker emits (η♯,φ)∈R check(η , )∈ R. Thus an approval-before-email monitor may prove the ordering while leaving account equality or approval freshness residual. Every accepted but unproved transition is therefore an explicit runtime obligation, as required by Section 6. 5. Dynamic Semantics The dynamic semantics is a small-step semantics over configurations: C=⟨e,H,τ⟩.C= e,H,τ . H is the handler stack and τ is the trace prefix. The active effect boundary ϵb _b and the effective policy monitor Π , compiled from TraceSpecAlgebra objects, are fixed parameters of the step relation for the current checked entry point: ϵb;Π⊢C⟶C′. _b; C C . We leave these parameters implicit in the rules. They are not mutable runtime state: ϵb _b restricts commits at the current checked boundary, and Π is advanced conceptually by replaying the trace prefix τ. Concrete deployment grants, tool exposure, and sandbox descriptors refine the implementation of dispatch, but they are not separate components of the core calculus. We write H⋅hH· h for the stack obtained by pushing handler frame h on top of H. 5.1. Expression Evaluation The small-step relation is call-by-value. Most rules apply under an evaluation context; dedicated action and handler rules update H or τ. Figure 11 combines the context grammar, core redexes, handler rules, and action-enforcement rules. trace eventsη::=(a)∣(a,h)∣(a)∣(j(a),ξ)evaluation contextsE::=[]∣Ee∣vE∣x=Ee∣Ee1e2∣c(v¯,E,e¯)∣eE∣h(E)∣h(E)∣E∣Efinish contextsG⊆E(G contains no h′ frame). array[]llcltrace events&η&::=& request(a) handled(a,h) commit(a) denied(j(a),ξ)\\[2.84526pt] evaluation contexts&E&::=&[\,] E\,e v\,E \ x=E\ in\ e\\ && &if\ E\ then\ e_1\ else\ e_2 \ c( v,E, e)\\ && &handle\ e\ with\ E _h(E) arm_h(E)\\ && &resume\ E \ E\\[2.84526pt] finish contexts&G& &E (G contains no scope_h frame). array E-Ctx ⟶⟨e,H,τ⟩⟨e′,H′,τ′⟩ ⟶⟨E[e],H,τ⟩⟨E[e′],H′,τ′⟩ E-Beta ⟶⟨(λx.e)v,H,τ⟩⟨e[↦xv],H,τ⟩ E-Let ⟶⟨=letxvine,H,τ⟩⟨e[↦xv],H,τ⟩ E-IfTrue ⟶⟨iftruethene1elsee2,H,τ⟩⟨e1,H,τ⟩ E-IfFalse ⟶⟨iffalsethene1elsee2,H,τ⟩⟨e2,H,τ⟩ E-Call =body(c)vf ⟶⟨callc(v1,…,vn),H,τ⟩⟨vfv1⋯vn,H,τ⟩ E-HandleEnter ⟶⟨handleewithh,H,τ⟩⟨scopeh(e),⋅Hh,τ⟩ E-HandleExit ⟶⟨scopeh(v),⋅Hh,τ⟩⟨v,H,τ⟩ E-FinishSkip ≠h′ ⟶⟨scopeh′(G[finishhv]),⋅Hh′,τ⟩⟨finishhv,H,τ⟩ E-FinishReturn ⟶⟨scopeh(G[finishhv]),⋅Hh,τ⟩⟨v,H,τ⟩ E-Perform-Handle =qrδΠ(qτ,request(a))∉qrBad=dispatchH(H,a)⟨h,u⟩ ⟶⟨performa,H,τ⟩⟨armh(u),H,⋅⋅τrequest(a)handled(a,h)⟩ E-Perform-Resume ⟶⟨armh(resumev),H,τ⟩⟨v,H,τ⟩ E-Perform-Finish ⟶⟨armh(finishv),H,τ⟩⟨finishhv,H,τ⟩ E-Perform-Commit =qrδΠ(qτ,request(a))∉qrBad ⪯nohandler(H,a)aϵb ∉δΠ(qr,commit(a))Bad=dispatchD(a)v ⟶⟨performa,H,τ⟩⟨v,H,⋅⋅τrequest(a)commit(a)⟩ E-Request-Deny ∈δΠ(qτ,request(a))Bad ⟶⟨performa,H,τ⟩⟨performError.raise⟨PolicyDenied⟩(a),H,⋅τdenied(request(a),PolicyDenied)⟩ E-Commit-Deny =qrδΠ(qτ,request(a))∉qrBad nohandler(H,a) a⋠∨ϵbδΠ(qr,commit(a))∈Bad ⟶⟨performa,H,τ⟩⟨performError.raise⟨PolicyDenied⟩(a),H,⋅⋅τrequest(a)denied(commit(a),PolicyDenied)⟩ gathered array[]@l@ E-Ctx\\[-1.05487pt] 3.99501pt $ $ 35.61961pt $ e,H,τ e ,H ,τ $ 46.40298pt $ E[e],H,τ E[e ],H ,τ $$ $ array 16.38895pt array[]@l@ E-Beta\\[-1.05487pt] 3.5pt $ $ $ true$ 53.85464pt $ (λ x.e)\,v,H,τ e[x v],H,τ $$ $ array\\[2.84526pt] array[]@l@ E-Let\\[-1.05487pt] 3.5pt $ $ $ true$ 66.22409pt $ \ x=v\ in\ e,H,τ e[x v],H,τ $$ $ array 16.38895pt array[]@l@ E-IfTrue\\[-1.05487pt] 3.5pt $ $ $ true$ 76.16956pt $ \ true\ then\ e_1\ else\ e_2,H,τ e_1,H,τ $$ $ array\\[2.84526pt] array[]@l@ E-IfFalse\\[-1.05487pt] 3.5pt $ $ $ true$ 76.67877pt $ \ false\ then\ e_1\ else\ e_2,H,τ e_2,H,τ $$ $ array 16.38895pt array[]@l@ E-Call\\[-1.05487pt] 3.60138pt $ $ 21.20966pt $ body(c)=v_f$ 71.46454pt $ \ c(v_1,…,v_n),H,τ v_f\,v_1\,·s\,v_n,H,τ $$ $ array\\[2.84526pt] array[]@l@ E-HandleEnter\\[-1.05487pt] 3.5pt $ $ $ true$ 84.10931pt $ \ e\ with\ h,H,τ _h(e),H· h,τ $$ $ array 16.38895pt array[]@l@ E-HandleExit\\[-1.05487pt] 3.5pt $ $ $ true$ 54.17834pt $ _h(v),H· h,τ v,H,τ $$ $ array\\[2.84526pt] array[]@l@ E-FinishSkip\\[-1.05487pt] 3.99501pt $ $ $ h≠ h $ 90.14554pt $ _h (G[finish_h\ v]),H· h ,τ _h\ v,H,τ $$ $ array 16.38895pt array[]@l@ E-FinishReturn\\[-1.05487pt] 3.5pt $ $ $ true$ 74.02289pt $ _h(G[finish_h\ v]),H· h,τ v,H,τ $$ $ array\\[2.84526pt] array[]@l@ E-Perform-Handle\\[-1.05487pt] 3.5pt $ $ 103.06331pt $ q_r= _ (q_τ, request(a)) 16.38895ptq_r∉ Bad 16.38895pt dispatchH(H,a)= h,u $ 102.34624pt $ \ a,H,τ arm_h(u),H,τ· request(a)· handled(a,h) $$ $ array\\[2.84526pt] array[]@l@ E-Perform-Resume\\[-1.05487pt] 3.5pt $ $ $ true$ 59.56761pt $ arm_h(resume\ v),H,τ v,H,τ $$ $ array 16.38895pt array[]@l@ E-Perform-Finish\\[-1.05487pt] 3.5pt $ $ $ true$ 70.71164pt $ arm_h(finish\ v),H,τ _h\ v,H,τ $$ $ array\\[2.84526pt] array[]@l@ E-Perform-Commit\\[-1.05487pt] 3.5pt $ $ 124.20265pt $ q_r= _ (q_τ, request(a)) 16.38895ptq_r∉ Bad$ $ nohandler(H,a) 16.38895pta _b$ 15.94449pt $ _ (q_r, commit(a))∉ Bad 16.38895pt dispatchD(a)=v$ 87.28262pt $ \ a,H,τ v,H,τ· request(a)· commit(a) $$ $ array\\[2.84526pt] array[]@l@ E-Request-Deny\\[-1.05487pt] 3.5pt $ $ 36.88937pt $ _ (q_τ, request(a))∈ Bad$ 159.61957pt $ \ a,H,τ \ Error.raise PolicyDenied (a),H,τ· denied( request(a), PolicyDenied) $$ $ array\\[2.84526pt] array[]@l@ E-Commit-Deny\\[-1.05487pt] 9.5pt $ $ 151.0445pt $ q_r= _ (q_τ, request(a)) 16.38895ptq_r∉ Bad$ 15.94449pt $ nohandler(H,a)$ 15.94449pt $ a _b\ \ _ (q_r, commit(a))∈ Bad$ 108.91718pt $ \ a,H,τ gatheredperform\ Error.raise PolicyDenied (a),H,\\[-0.75346pt] τ· request(a)· denied( commit(a), PolicyDenied) gathered $$ $ array gathered Figure 11. Call-by-value dynamic semantics over ⟨e,H,τ⟩ e,H,τ . The figure gives trace events and contexts, then pure, call, handler, action-enforcement, and denial rules. Handled actions record request and handled events; unhandled actions commit only after request, boundary, and commit-monitor checks. Rejected requests or commits append denial events and raise PolicyDenied, preserving the request/handle/commit distinction. Concrete trace events, evaluation and finish contexts, followed by small-step rules for pure reduction, checked calls, handler scopes, handled and committed actions, and policy denial. The ordinary contexts evaluate the handler position of eehhandle\ e\ with\ e_h, but they do not evaluate the handled body before the dynamic handler scope is installed. The rules in Section 5.4 push a handler frame and introduce the administrative delimiter h(e)scope_h(e); evaluation then continues inside that scoped body. Handler arms reuse the ordinary small-step relation until they reach vresume\ v or vfinish\ v, so arm-local lets, conditionals, and calls are covered by the same rules as ordinary expressions. Source loops elaborate to recursive checked callables and require no additional core redex. No separate arm-evaluation relation is needed. Rule E-Perform-Handle places the selected body in the administrative frame h(e) arm_h(e), where it takes ordinary small steps. Since resume and finish are terminal in an arm, the two exit rules consume them at that arm. The enclosing evaluation context is the suspended single-shot continuation: resume replaces the original perform redex by its value, while finish creates the targeted form hvfinish_h\ v. E-FinishSkip discards a scope-free finish context G, including any intervening arm frames, and crosses a non-target handler scope. E-FinishReturn discards the final G and returns at the matching delimiter. Calls to checked callables use E-Call. The meta-level lookup (c) body(c) returns the unary function value associated with the callable descriptor c, whether that descriptor was generated from a source flow, an agent method such as Reviewer.run, a tool wrapper, or a standard-library binding. If c has multiple entry arguments, the stored body is a nest of unary abstractions and E-Call turns the checked call into a left-associated sequence of ordinary applications. Model nondeterminism appears only when such a body performs an . Agentic.infer action. 5.2. Actions and Traces We use two enforcement phases for a concrete action a. Request enforcement decides whether the program may ask for the typed action at the current trace prefix. Commit enforcement decides whether the default runtime implementation may actually perform the external side effect. The split is what makes handled actions persistent in the audit trace without forcing them to escape to the caller. In Figure 11, qτq_τ is the monitor state reached by replaying τ, and qr=δΠ(qτ,(a))q_r= _ (q_τ, request(a)) is the state after the request. Request enforcement succeeds only when qr∉q_r∉ Bad. If a handler matches, E-Perform-Handle records the request and handled outcome before evaluating the selected arm. Otherwise, E-Perform-Commit additionally requires a⪯ϵba _b and an accepted commit transition before invoking the default implementation. The rules append events only after these premises succeed. The implementation may add deployment-grant, tool-exposure, or sandbox predicates to these checks. The core rules omit them because they do not change the proof obligations: they only make request or commit enforcement more restrictive. The policy trace records request, handled, commit, and denial events. An arm’s resume or finish is represented by its terminal outcome rather than by another policy event; an implementation may retain that distinction as diagnostic metadata. The action redex is written directly as aperform\ a. Figure 11 first enters the selected arm and then separates its terminal outcomes. E-Perform-Resume fills the suspended action site. E-Perform-Finish unwinds to the handled-expression delimiter. In the handled-action rules, (H,a) dispatchH(H,a) returns the nearest matching handler frame and the selected arm body after binding the concrete action payload to the clause parameters. The predicate (H,a) nohandler(H,a) selects the complementary path; (a)=v dispatchD(a)=v then invokes the registered default implementation and returns its value. If enforcement fails, the semantics raises a typed error action and records a denial event. E-Request-Deny covers a rejected request; E-Commit-Deny covers either a rejected commit transition or an action outside ϵb _b. Both use PolicyDenied as the core typed error; implementations may refine the diagnostic with deployment-grant, sandbox, schema, or tool-exposure causes. Agent-scoped inference is a distinguished action, not a separate core redex. Its surface elaboration is: ⟦⟨T⟩(p)⟧g=.⟨g,T⟩(p). \ infer T (p) _g=perform\ Agentic.infer g,T (p). Its provider nondeterminism, output-schema validation, model-selected tool calls, metadata, and token consumption are part of default dispatch for that action. Each requested tool call is mediated as an action; no model output can cause an unmediated host operation. If output validation fails, dispatch raises .⟨⟩ Error.raise SchemaError and records the failure. Retries are represented by ordinary source-level control around the inference operation and do not change the meaning of the model relation. 5.3. Runtime Policy Enforcement Runtime policy enforcement is prefix-based. Before a request or commit event is appended, the monitor compiled from the effective TraceSpecAlgebra object is advanced on that event. If the resulting state is in Bad, the corresponding request or commit is not authorized; the trace records a denied request or denied commit instead. The denial rules in Figure 11 are the failure counterparts of the monitor and effect-boundary premises in the action rules. These rules are the dynamic counterpart of the static automata analysis in Section 4.4. Static proof can remove a check only when the compiler can show that all abstract prefixes accepted by the program remain outside Bad. Otherwise, the residual check remains explicit as a runtime enforcement obligation. Effect boundaries. An effect boundary is a runtime contract for an entry point or checked callable boundary. It constrains the actions that may commit through the default runtime implementation and therefore escape the boundary as real external side effects. In the core relation, ϵb _b is fixed for the checked boundary currently being evaluated. A nested checked call can be modeled by evaluating the callee under a smaller boundary, but this is an indexed-judgment change rather than mutable runtime state. Because boundaries narrow rather than widen commit authority, callees cannot acquire external actions unavailable to their callers. A local handler may still interpret a request as a dry run, mock result, or recovery path; that interpretation records a handled event rather than a commit event. Implementation refinements and recovery. Deployments may strengthen core enforcement with tool-exposure, grant, and sandbox predicates; these checks only reject additional requests or commits. The resulting trace also guides recovery: deterministic computations may be recomputed, whereas agent calls, external reads, approvals, and non-idempotent writes are replayed from checkpoints. Resampling a model call is distinct from replay and requires explicit policy authorization. 5.4. Handlers Handlers interpret selected action requests after request enforcement succeeds. The nearest matching frame records a handled event and evaluates its arm; resume fills the suspended action site, whereas finish supplies the result of the handled expression. With no matching frame, execution proceeds through commit enforcement to the default dispatcher. Installing a handler changes neither ϵb _b nor Π : it may make a request non-escaping, but it cannot create authority to commit an action rejected by the boundary or monitor. 6. Soundness This section states the safety properties targeted by the design. The prototype currently implements the corresponding checks as compiler and interpreter invariants; a mechanized proof is future work. We separate two layers of metatheory. First, ordinary type safety ensures that the core calculus is well behaved: well-typed closed programs preserve their result type as they step and do not get stuck. Second, the agent-language-specific theorems connect the same typing derivations to effects, traces, policies, and handlers. 6.1. Auxiliary Notions Let α(a)α(a) be the abstraction of a concrete action a to an effect pattern, and let a⪯ϵa ε mean that α(a)α(a) is covered by effect row ϵε, using Ξ for any spec-bound resource predicates in the pattern. Let (τ) reqs(τ) be the sequence of actions that appear in request events, and let (τ) commits(τ) be the sequence of actions that appear in commit events, ignoring checkpoint and resume metadata. Let A⊧τA τ mean that concrete trace τ is represented by abstract requested-action trace A. Let MΠM_ be the monitor denoted by the effective environment Π , which is obtained by compiling TraceSpecAlgebra objects. We write A′⊑A A for language inclusion between requested-action abstractions, and ϵ′⊑ϵε ε for effect-row inclusion. We say that a configuration C=⟨e,H,τ⟩C= e,H,τ is well formed under ϵb;Π _b; when the expression is well typed, the active effect boundary covers the entry declaration, handlers in H have well-typed arms, and all residual policy checks inserted by the compiler are present in the interpreter plan. Resource markers are ordinary types, and their facts are checked through action signatures and type-spec evidence rather than as separate mutable components of the core configuration. 6.2. Basic Type Safety The standard preservation/progress facts are stated for closed Core Etas configurations whose callable, action, handler, and spec summaries are well formed in Ξ . Runtime policy denial and abort are not stuck states: denial becomes a typed error action, while abort is an explicit terminal outcome. Lemma 1 (Preservation). Assume well-formed Ξ and Π , and suppose Ξ;∅;Π⊢e⇒τ!ϵ⊳A⊣R⟨e,H,θ⟩⟶⟨e′,H′,θ′⟩. ; ; e τ !ε A R e,H,θ e ,H ,θ . If the initial configuration is well formed and contains the residual checks R, then there exist ϵ′ε , A′A , and R′R such that Ξ;∅;Π⊢e′⇒τ!ϵ′⊳A′⊣R′ϵ′⊑ϵA′⊑AR′⊆R. ; ; e τ !ε A R ε ε A A R R. Moreover, H′H is well formed and any trace event appended by the step is represented by A. Proof sketch. By case analysis on the small-step rule. Pure computation rules E-Beta, E-Let, E-IfTrue, and E-IfFalse use the substitution lemma for ordinary values. Checked calls use the callable summary in Ξ , so expanding c(v¯)call\ c( v) to the associated unary function application preserves the declared result type and summary bound. Handler rules push, pop, or unwind only H; the typing rule for handle already accounts for the effects produced by arms. Action rules, including inference actions, append request, handled, denied, or commit events only at redexes introduced by the corresponding typing rules, and residual checks are consumed only after their guarded dynamic test has succeeded. ∎ Lemma 2 (Progress). Assume well-formed Ξ , Π , handler stack H, and trace prefix θ. If Ξ;∅;Π⊢e⇒τ!ϵ⊳A⊣R ; ; e τ !ε A R and the runtime plan contains the residual checks R, then exactly one of the following holds: (i)e is a value;(i)e is an explicit enforcement terminal;(i)∃e′,H′,θ′.⟨e,H,θ⟩⟶⟨e′,H′,θ′⟩. array[]l(i)&e is a value;\\ (i)&e is an explicit enforcement terminal;\\ (i)&∃ e ,H ,θ .\ e,H,θ e ,H ,θ . array Here enforcement terminals include schema failure and abort outcomes produced by the dynamic semantics. Policy denial instead takes a step to the typed .⟨⟩ Error.raise PolicyDenied action. Proof sketch. By induction on the typing derivation. Values are immediate. Elimination forms either contain a non-value subexpression, in which case the evaluation-context rule applies by the induction hypothesis, or contain values and match a redex rule. A performed action either finds a matching handler, passes through the default dispatcher, or is rejected by policy, boundary, or schema enforcement. The last case is progress: the semantics produces a typed enforcement terminal rather than becoming stuck. The arm typing rules ensure that handler arms cannot fall through; they end in resume, finish, or an explicit abort. ∎ Theorem 3 (Type soundness). If a closed expression e is well typed under well-formed Ξ and Π , and execution starts from a well-formed runtime configuration containing the residual checks produced by typing, then no reachable configuration is stuck. Proof sketch. By induction on the length of the multi-step execution, using Lemma 1 to re-establish typing after each step and Lemma 2 to show that each reachable non-value, non-terminal configuration can take a step. ∎ 6.3. Effect and Trace Soundness Effect soundness states that the escaping row is a genuine upper bound on committed external behavior, while the requested-action abstraction is a genuine upper bound on requested trace behavior. The theorem deliberately does not require every requested action to be covered by the escaping row, because a handler may make a request non-escaping. Theorem 4 (Effect soundness). Assume well-formed Ξ and Π , assume Ξ;Γ;Π⊢e⇒τ!ϵ⊳A⊣R ; ; e τ !ε A R, and assume an initial well-formed configuration ⟨e,H,τ0⟩⟶∗⟨v,H′,τ1⟩. e,H, _0 ^* v,H , _1 . Then: ∀a∈(τ1)∖(τ0).a⪯ϵ∨(a,ϵ),A⊧(τ1∖τ0). array[]l∀ a∈ commits( _1) commits( _0).\ a ε residCov(a,ε),\\[2.84526pt] A ( _1 _0). array Here (a,ϵ) residCov(a,ε) means that a is a compiler-inserted residual check whose guarded action is covered by ϵε. Proof sketch. By induction on the small-step derivation. Pure rules add no actions. Rules for checked callable calls and perform append request events introduced by T-Call and T-Action through the static signature Ξ . Callable descriptors and action signatures contribute their boundary events through summaries rather than through ad hoc core redexes. Commit events arise only through default dispatch after commit enforcement, so their abstractions are covered by the escaping row or by a compiler-inserted residual check. The handler rule may remove handled effects from the escaping row, but the typing rule preserves the handled computation’s requested-action abstraction. Residual checks in R are inserted by the monitor-discharge judgment precisely at points where the static event pattern is known but the concrete parameter is dynamic. ∎ 6.4. Policy Safety Policy safety states that a program accepted by the typing judgment cannot request or commit an action event that violates the effective monitor compiled from active trace specs. The theorem is stated with residual checks because Etas intentionally permits policies whose resource predicates depend on runtime values. Theorem 5 (Policy safety). Assume Ξ;Γ;Π⊢e⇒τ!ϵ⊳A⊣R ; ; e τ !ε A R. Suppose execution starts from a well-formed configuration that contains R, and suppose every residual check is enforced before its guarded request or commit event. Then every prefix of the produced trace is accepted by MΠM_ : ∀τ′.τ′⪯τ1⇒MΠ(τ′)∉.∀τ .\ τ _1 M_ (τ )∉ Bad. Proof sketch. The trace-spec premises inside typing normalize source specs to monitors; the monitor-discharge premises then either prove an event transition accepted, make the typing rule inapplicable, or emit a residual check in R. For proved transitions, soundness of the abstraction ensures that all concrete events represented by the abstract event keep the monitor outside Bad. For residual transitions, the dynamic denial rules prevent the request or commit whenever the concrete monitor transition would enter Bad. Since enforcement is prefix-based and every request and commit is mediated before its event is appended, the property holds for all trace prefixes. ∎ 6.5. Handler Transparency Handlers should not hide requests or create commit authority. This is the key difference between Etas handlers and unrestricted algebraic effect handlers. Theorem 6 (Handler trace transparency). Installing a well-typed handler frame may remove handled effects from the escaping row, but it does not remove the corresponding request events from the requested-action trace. If a handled computation requests action a, the produced trace contains (a) request(a) followed by a handled outcome. If a handler or default dispatcher commits a, then a passes the same boundary and policy checks that would be required without the handler frame. Proof sketch. The E-HandleEnter rule pushes the handler frame onto H, and E-HandleExit/E-FinishReturn restore the previous stack when the scoped computation returns or finishes. The E-Perform-Handle rule appends request and handled events before the arm runs, so either terminal arm outcome remains auditable. The E-Perform-Commit rule is the only rule that appends a commit event, and its premises include commit enforcement. Therefore a handler can affect the interpretation of a request but cannot manufacture commit authority. ∎ Taken together, these theorems do not assert that model outputs are correct, stable, or safe. They establish a narrower property: whatever the model returns, the surrounding program cannot commit an undeclared, unauthorized, or unmonitored external action without crossing an explicit residual check or raising a typed enforcement error, and it cannot erase a handled request from the audit trace. This is the level at which a programming language can improve agent-system reliability without treating model alignment as a type-system property. 7. Implementation The current Etas prototype is implemented in Rust across component repositories composed by a user-facing distribution workspace. Its CLI composes component repositories for syntax, HIR, types, effects, standard library metadata, host bindings, and interpretation. This structure reflects the language design: the user sees one tool, while compiler and interpreter responsibilities remain separated. 7.1. Compiler Pipeline The implemented pipeline is: →→. source→ AST→ HIR→ checked\ HIR→ interpreter. The frontend parses source, lowers declarations and bodies to source-shaped HIR, resolves imports and names, checks types and effects, analyzes loop progress, and verifies interpreter support. Its output is a CheckedProject containing HIR together with the type, effect, requested-action, source-map, and entry-point facts needed downstream. The interpreter consumes this checked project directly. Before evaluation, it derives an interpreter plan containing slot layouts, globals, resources, intrinsic dispatch, host requirements, and action-mediation metadata. This plan is execution metadata over HIR, not another language representation. Direct HIR interpretation keeps diagnostics and interpreter events connected to source spans while the language is still evolving. 7.2. Effect, Trace-Spec, and Handler Diagnostics The checker treats effect, trace-spec, and policy-monitor failures as first-class diagnostics. Negative tests are expected to report targeted errors rather than generic “not implemented” messages. This matters for the design because the language is useful only if programmers can understand why an action row is too narrow, a trace-spec obligation cannot be proved, a model-callable tool hides high-impact effects, or a handler attempts to resume illegally. Package metadata is part of the same story. Imported modules and host bindings must expose public type, effect, action, tool, and trace-spec contracts, allowing downstream code to check effects and requested traces without seeing every implementation body. This resembles separate compilation for ordinary types; the exported interface also carries authority and TraceSpecAlgebra summaries. 7.3. Checked-HIR Interpreter Interpreter::run_checked accepts a CheckedProject, an entry point and arguments, host services, and run options. It first builds and validates the interpreter plan, including host-readiness and action-mediation facts, then evaluates HIR with explicit frames, slots, control signals, and single-shot continuations. Flow and agent calls, handlers, checkpoints, and resume are therefore interpreter behavior over checked HIR. Runtime limits and retry budgets are implemented as orthogonal interpreter facilities; they are not part of the Core Etas formalism. Pure intrinsics execute locally. Model, tool, memory, approval, console, and command boundaries are converted to typed requests and routed through supplied host services. The result contains an interpreter value or diagnostics, together with workflow events and checkpoints. This implementation provides the compiler-and-interpreter baseline evaluated in this paper; a separate optimization representation and production scheduler are outside the current prototype. 8. Evaluation The evaluation of Etas should answer four questions. RQ1: Expressiveness.: Can the language express representative agent-system patterns without encoding the safety-relevant structure outside the language? RQ2: Static detection.: Do effect, policy, prompt-trust, memory, and handler checks catch the intended classes of mistakes at compile time? RQ3: Runtime evidence.: Does mediated execution produce traces that are sufficient for audit, replay, recovery, and residual policy enforcement? RQ4: Optimization.: Does checked program structure expose enough evidence to justify agent-specific rewrites without weakening effects or trace specs? The current prototype supports an artifact-oriented evaluation through case-study programs, compiler diagnostics, and interpreter traces. We use these artifacts to examine whether safety-relevant structure remains visible to static checking, runtime audit, and optimization discovery. 8.1. Case Studies Recent agent practice has converged on three recurring engineering problems. Context engineering generalizes prompt engineering into the systematic selection, processing, and management of the information made available to a model at inference time (Mei et al., 2025); in software agents, project-specific context files already encode architecture, interfaces, workflows, and local policies (Mohsenimofidi et al., 2026). Harness engineering concerns the runtime substrate around the model: tool surfaces, retrieval strategy, tool-result presentation, structured outputs, validation, retries, and evaluation harnesses. Recent search experiments show that accuracy can depend strongly on the harness and tool-calling style even when the underlying data are fixed (Sen et al., 2026). Loop engineering is the emerging practice of designing recurring agent systems that keep working until a goal, budget, or acceptance predicate is reached; recent hands-free agent loops combine executable evaluators, isolated worktrees, git policies, tracing, and replay (Yu et al., 2026), and practitioner accounts identify automations, worktrees, skills, connectors, and subagents as the loop substrate (Griffiths, 2026). ⬇ spec PublicContext: trace = +Memory.read<ProjectMemory.Reports> & +Web.search<_> & -Memory.read<ProjectMemory.Secrets>; flow BuildContext(req: DraftRequest) → Prompt ~ PublicContext let prior = ProjectMemory.Reports.get(req.related); let hits = search_web(req.topic); return Prompt.new() .system(Trusted("Use approved context only.")) .data( request = req, prior, hits ); (a) Context engineering. ⬇ spec TriageHarness: trace = +Web.search<_> & -Shell.exec<_> & +Tickets.write<Sandbox>; @model("GPT-5.5") @tools([search_web, update_ticket]) @limits([Tokens(8000), Attempts(2)]) agent Triage(req: Ticket) → TriageDecision ~ TriageHarness let d = perform infer<TriageDecision>( BuildTicketContext(req)); update_ticket(req.id, d.summary); return d; (b) Harness engineering. ⬇ spec RepairLoop: trace = +Repo.checkout<IsolatedWorktree> & +CI.run<Project> & +Review.request & +Repo.merge<ProtectedMain> & (CI.run<Project> >> Repo.merge<ProtectedMain>) & (Review.request >> Repo.merge<ProtectedMain>); flow repair(goal: Issue) → Patch ~ RepairLoop let wt = perform Repo.checkout<IsolatedWorktree>(goal.repo); for round in std.range(6) limit Attempts(6), Tokens(60000) do let patch = RepairAgent.run( goal, wt, round ); let test = perform CI.run<Project>(wt, patch); if test.ok && std.ui.approve("merge?", patch, risk = High) perform Repo.merge<ProtectedMain>(wt, patch); return patch; abort("repair budget exhausted"); (c) Loop engineering. ⬇ @model("gpt-5.5") @tools([web.search, paper.search, repo.read, db.query]) agent Researcher(input: ResearchTask) → ResearchResult return perform infer<ResearchResult>( ResearchPrompt(input)); spec LiteratureOnly: trace = +PaperSearch.search<_> & -WebSearch.search<_> & -Repo.read<_> & -Db.query<_>; flow literature_batch(task: ResearchBatch) → Array<ResearchResult> ~ LiteratureOnly var results = []; for q in task.questions limit Tokens(30000) do let papers = paper.search(task.topic); results = results.push(Researcher.run( question = q, papers )); return results; // derived optimization plan: // hoist/dedup paper.search(task.topic) // parallelize independent questions // expose only paper.search (d) Optimization. Figure 12. Four language-visible agent-engineering cases. The left column stacks context engineering (a), which excludes secret memory from a typed prompt, and harness engineering (b), which fixes the model, tools, budget, and allowed actions. The middle column gives loop engineering (c): an isolated repair loop must observe CI and review before protected merge. The right column demonstrates an effect- and trace-aware optimization plan (d). The call-site spec narrows a four-tool agent to paper search; a stable, loop-invariant search is hoisted and deduplicated; and independent research iterations may run concurrently while preserving result order and their shared token limit. Token and attempt bounds are operational, while the effect, trace, and specialization facts that justify these rewrites are statically visible. Four Etas examples arranged in three columns. Context and harness examples are stacked in the left column; a bounded repair loop occupies the middle; the right column combines tool-surface specialization, stable retrieval hoisting, deduplication, and conflict-free parallel scheduling. The budget annotations in Figure 12(b–c) exercise orthogonal interpreter facilities and are not constructs of the Core Etas formal development. Figure 12 presents code snippets extracted from four programs supported by our Etas implementation. Context engineering. Figure 12(a) treats the prompt context as a typed program artifact rather than as an unstructured string assembled in callbacks. The effect row states which context sources may be queried, and the trace spec denies secret memory regions while admitting approved report memory and web search. This makes a case study measurable in two ways: the compiler can reject secret leakage before execution, and the interpreter trace can explain which sources entered a model call when an output is audited. Harness engineering. Figure 12(b) packages the agent harness into source-level semantics: model choice, tool exposure, structured output type, allowed tool actions, and an implementation-level runtime budget all appear in the program. The interesting comparison is not whether a framework can run the same workflow, but whether the harness is visible to static analysis. In Etas, the compiler can warn if the exposed tool set contains a dangerous action such as shell execution, insert residual checks when a ticket destination is only known at runtime, and use handlers to run the same harness in dry-run or mock mode without erasing the requested actions from the trace. Loop engineering. Figure 12(c) represents a recurring repair loop as a bounded program constrained by trace specs. The loop is allowed to operate only in an isolated worktree, can run CI repeatedly under an interpreter-enforced budget, and can merge only after both CI and review have appeared earlier in the trace. This gives the language concrete static-safety and audit hooks: the compiler rejects definite ordering violations, while the interpreter enforces the runtime budget and records the actions and checkpoints needed to audit each iteration. Answer to RQ1: Expressiveness. Yes, for the evaluated patterns. Figure 12(a–c) expresses model boundaries, tool exposure, typed context and memory, approval ordering, and runtime limits in source declarations and specs rather than external callback conventions. This evidence covers three compact patterns, not general claims about large-program ergonomics. Answer to RQ2: Static detection. Yes for the modeled properties, with residualization. Across the cases, the checker infers effects and requested actions and rejects definite secret-memory, shell, ordering, and handler violations. Predicates depending on concrete runtime resources remain explicit residual checks rather than being silently accepted or rejected. Answer to RQ3: Runtime evidence. Yes at prototype scope. Checked-HIR execution emits request, handled, commit, denial, workflow, budget, and checkpoint evidence sufficient to audit these runs and drive the implemented replay and recovery hooks. The case studies do not yet establish trace completeness at production scale. 8.2. Optimization Figure 12(d) combines three optimizations from the language examples. First, package metadata connects tools to action signatures, so LiteratureOnly narrows Researcher’s four-tool surface to .\ paper.search\. Second, paper.search(task.topic) is loop invariant; when its action summary marks the result stable within the run with topic as its cache key, the search can be hoisted and one traced result can serve all iterations. Third, the remaining Researcher.run calls have no data dependence or conflicting escaping effects. They may therefore be scheduled concurrently when the monitor admits either order, with results restored to source order and the shared token limit preserved. Answer to RQ4: Optimization. Yes. The current frontend records tool metadata, specialized action summaries, spec conformance, and source-shaped loop structure in checked HIR, which is sufficient to identify these candidates and their side conditions. Because Etas makes stability, effect conflict, trace equivalence, and limit preservation compiler-visible, this information will enable an optimizer to apply rewrites and improve runtime performance. 9. Related Work Effects, handlers, and authority. Algebraic effects and handlers separate operation interfaces from their interpretations (Plotkin and Power, 2003; Plotkin and Pretnar, 2013; Bauer and Pretnar, 2015); Koka shows that row-typed effects can be inferred and compiled efficiently (Leijen, 2014, 2017). Related systems study row-polymorphic and direct-style handlers, effect abstraction, handler names, and refinement reasoning (Hillerström and Lindley, 2016; Lindley et al., 2017; Biernacki et al., 2019; Xie et al., 2022; Kawamata et al., 2024). Etas adopts rows and first-class handlers but retains a typed requested-action trace after handling: a handler may remove an escaping obligation, but cannot erase the request or grant commit authority. This design also connects scope-based capability accounts with type-based effects (Brachthäuser et al., 2022): tool exposure limits which actions an agent can request, while effects and specs mediate the concrete commit. Trace enforcement and information flow. Security automata characterize enforceable trace properties (Schneider, 2000). Etas compiles kinded trace specs to such monitors, but first uses effect inference and abstract requested traces to discharge provable obligations; residual monitors handle resource values and model-selected arguments known only at runtime. Events distinguish requests, handled outcomes, denials, and commits, so local interpretation remains auditable. Prompt trust is related to information-flow control (Denning, 1976), but targets the narrower problem of exposing untrusted or secret flows into privileged model inputs without requiring a full dependent information-flow system. Agent and coordination models. Reward-guided synthesis treats agent control structures as synthesized programs (Cui et al., 2024); Etas instead provides the checked programming model around inference, tools, memory, approval, traces, replay, and secondary runtime limits. Choreographies make coordination explicit through projection and communication structure (Giallorenzo et al., 2024; Bates et al., 2025), while session types govern protocol progression (Honda et al., 1998). Etas shares their insistence on explicit structure, but targets model-backed agents, tool authority, and trace enforcement rather than endpoint projection or deadlock freedom. Its implementation also differs from optimization DSLs such as Allo (Chen et al., 2024): the current compiler attaches types, effects, and action summaries to source-shaped HIR and interprets it directly, without a separate schedule or optimization IR. This matters for agent runtimes because authority can change between request and commit. Etas therefore preserves the provenance of requested actions even when handlers, deployment grants, or scheduler choices decide whether an external action actually occurs. This keeps optimization tied to the same policy evidence used for enforcement, rather than treating scheduling as a separate correctness argument. 10. Conclusion This paper presents Etas, a programming-language for agent systems in which model-backed inference, tool calls, prompts, memory, approvals, policies, handlers, and traces are explicit semantic objects rather than framework conventions. The design separates deterministic computation from agentic nondeterminism and separates escaping effects from the persistent requested-action trace, allowing handlers to support testing, replay, recovery, and host adaptation without hiding the authority that a program requested. Its static semantics combines ordinary typing with spec conformance, TraceSpecAlgebra monitors, abstract trace discharge, and residual runtime obligations; its dynamic semantics mediates every request and commit through policy, effect-boundary, deployment, and sandbox checks; and its soundness statements identify the resulting guarantees for types, effects, traces, policy safety, and handler transparency. Our Etas prototype and artifact-oriented evaluation show that these ideas can be implemented as compiler diagnostics, checked-HIR execution, trace-aware runtime plans, fixture tests, and case studies for context, harness, and loop engineering. The broader conclusion is that agent-system safety and auditability need not be recovered from callbacks and logs after the fact: they can be made part of the language interface that programmers write, compilers check, and runtimes enforce. References (1) Bates et al. (2025) Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, and Joseph P. Near. 2025. Efficient, Portable, Census-Polymorphic Choreographic Programming. Proc. ACM Program. Lang. 9, PLDI, Article 193 (June 2025), 24 pages. doi:10.1145/3729296 Bauer and Pretnar (2015) Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming 84, 1 (Jan. 2015), 108–123. doi:10.1016/j.jlamp.2014.02.001 Biernacki et al. (2019) Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2019. Abstracting algebraic effects. Proc. ACM Program. Lang. 3, POPL, Article 6 (Jan. 2019), 28 pages. doi:10.1145/3290319 Brachthäuser et al. (2022) Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki. 2022. Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back. Proc. ACM Program. Lang. 6, OOPSLA1, Article 76 (April 2022), 30 pages. doi:10.1145/3527320 Chen et al. (2024) Hongzheng Chen, Niansong Zhang, Shaojie Xiang, Zhichen Zeng, Mengjia Dai, and Zhiru Zhang. 2024. Allo: A Programming Model for Composable Accelerator Design. Proc. ACM Program. Lang. 8, PLDI, Article 171 (June 2024), 28 pages. doi:10.1145/3656401 CloudWeGo (2026) CloudWeGo. 2026. Eino User Manual. https://w.cloudwego.io/docs/eino/ Accessed: 2026-06-17. Cousot and Cousot (1977) Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California) (POPL ’77). Association for Computing Machinery, New York, NY, USA, 238–252. doi:10.1145/512950.512973 CrewAI (2026) CrewAI. 2026. CrewAI Documentation. https://docs.crewai.com/ Accessed: 2026-06-17. Cui et al. (2024) Guofeng Cui, Yuning Wang, Wenjie Qiu, and He Zhu. 2024. Reward-Guided Synthesis of Intelligent Agents with Control Structures. Proc. ACM Program. Lang. 8, PLDI, Article 217 (June 2024), 25 pages. doi:10.1145/3656447 Denning (1976) Dorothy E. Denning. 1976. A lattice model of secure information flow. Commun. ACM 19, 5 (May 1976), 236–243. doi:10.1145/360051.360056 Giallorenzo et al. (2024) Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. 2024. Choral: Object-oriented Choreographic Programming. ACM Trans. Program. Lang. Syst. 46, 1, Article 1 (Jan. 2024), 59 pages. doi:10.1145/3632398 Griffiths (2026) Brent D. Griffiths. 2026. Forget prompt engineering: ‘Loop engineering’ is all the rage now. https://w.businessinsider.com/what-are-loops-ai-engineering-tips-2026-6 Accessed: 2026-07-03. Hillerström and Lindley (2016) Daniel Hillerström and Sam Lindley. 2016. Liberating effects with rows and handlers. In Proceedings of the 1st International Workshop on Type-Driven Development (Nara, Japan) (TyDe 2016). Association for Computing Machinery, New York, NY, USA, 15–27. doi:10.1145/2976022.2976033 Honda et al. (1998) Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. In Programming Languages and Systems, Chris Hankin (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 122–138. Kammar et al. (2013) Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (Boston, Massachusetts, USA) (ICFP ’13). Association for Computing Machinery, New York, NY, USA, 145–158. doi:10.1145/2500365.2500590 Kawamata et al. (2024) Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, and Tachio Terauchi. 2024. Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. Proceedings of the ACM on Programming Languages 8, POPL, Article 5 (2024), 33 pages. doi:10.1145/3633280 LangChain (2026) LangChain. 2026. LangGraph Overview. https://docs.langchain.com/oss/python/langgraph/overview Accessed: 2026-06-17. Leijen (2014) Daan Leijen. 2014. Koka: Programming with Row Polymorphic Effect Types. Electronic Proceedings in Theoretical Computer Science 153 (June 2014), 100–126. doi:10.4204/eptcs.153.8 Leijen (2017) Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL ’17). Association for Computing Machinery, New York, NY, USA, 486–499. doi:10.1145/3009837.3009872 Lindley et al. (2017) Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL ’17). Association for Computing Machinery, New York, NY, USA, 500–514. doi:10.1145/3009837.3009897 Mei et al. (2025) Lingrui Mei, Jiayu Yao, Yuyao Ge, Yiwei Wang, Baolong Bi, Yujun Cai, Jiazhi Liu, Mingyu Li, Zhong-Zhi Li, Duzhen Zhang, Chenlin Zhou, Jiayi Mao, Tianze Xia, Jiafeng Guo, and Shenghua Liu. 2025. A Survey of Context Engineering for Large Language Models. arXiv:2507.13334 [cs.CL] https://arxiv.org/abs/2507.13334 Microsoft (2026a) Microsoft. 2026a. Agent Framework Documentation. https://learn.microsoft.com/en-us/agent-framework/ Accessed: 2026-06-17. Microsoft (2026b) Microsoft. 2026b. AutoGen Documentation. https://microsoft.github.io/autogen/stable/ Accessed: 2026-06-17. Mohsenimofidi et al. (2026) Seyedmoein Mohsenimofidi, Matthias Galster, Christoph Treude, and Sebastian Baltes. 2026. Context Engineering for AI Agents in Open-Source Software. arXiv:2510.21413 [cs.SE] https://arxiv.org/abs/2510.21413 OpenAI (2026) OpenAI. 2026. OpenAI Agents SDK Documentation. https://openai.github.io/openai-agents-python/ Accessed: 2026-06-17. Plotkin and Power (2003) Gordon Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. Applied Categorical Structures 11, 1 (2003), 69–94. doi:10.1023/A:1023064908962 Plotkin and Pretnar (2013) Gordon D Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Logical Methods in Computer Science 9, 4, Article 23 (Dec. 2013), 36 pages. doi:10.2168/lmcs-9(4:23)2013 Schneider (2000) Fred B. Schneider. 2000. Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3, 1 (Feb. 2000), 30–50. doi:10.1145/353323.353382 Sen et al. (2026) Sahil Sen, Akhil Kasturi, Elias Lumer, Anmol Gulati, and Vamse Kumar Subbiah. 2026. Is Grep All You Need? How Agent Harnesses Reshape Agentic Search. arXiv:2605.15184 [cs.CL] https://arxiv.org/abs/2605.15184 Xie et al. (2022) Ningning Xie, Youyou Cong, Kazuki Ikemori, and Daan Leijen. 2022. First-class names for effect handlers. Proc. ACM Program. Lang. 6, OOPSLA2, Article 126 (Oct. 2022), 30 pages. doi:10.1145/3563289 Yu et al. (2026) Cunxi Yu, Chenhui Deng, Nathaniel Pinckney, and Brucek Khailany. 2026. Agentic Hardware Design as Repository-Level Code Evolution. arXiv:2606.28279 [cs.AR] https://arxiv.org/abs/2606.28279