Pith. sign in

REVIEW 3 major objections 4 minor 30 references

ETAS makes agent actions, policies, and traces first-class program elements, checked before and during execution.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 17:03 UTC pith:HZ6DEE3Q

load-bearing objection A genuinely new design for typed agent authorization, with a real gap between the stated policy-safety theorem and the formal dynamic semantics — worth engaging, but not as-is. the 3 major comments →

arxiv 2607.17780 v1 pith:HZ6DEE3Q submitted 2026-07-20 cs.PL cs.AIcs.LGcs.MA

ETAS: An Effect-Typed Language for Agent Systems

Huiri Tan , Yikun Wang , Puyang Zhang , Shangyu Li , Jiasi Shen This is my paper
classification cs.PL cs.AIcs.LGcs.MA MSC 68N3068Q60
keywords agent systemseffect typestrace specspolicy enforcementhandlersauditabstract interpretationprogramming languages
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

ETAS is a programming language that treats an agent system as a program with semantic structure, not as host-language callbacks around prompts and tools. The paper's central claim is that authorization, nondeterminism, recovery behavior, and audit evidence can be reasoned about before and during execution, even when handlers make requested effects non-escaping. It achieves this by tracking two separate behavioral summaries for every computation: an escaping effect row (obligations left to the caller) and a persistent requested-action trace (what the program asked for, regardless of whether a handler intercepted it). Trace specs written as source-level constraints compile into monitors, and the type checker either proves the requested trace safe, rejects it, or emits explicit residual runtime checks. If the design works as claimed, agent safety becomes a property of the language interface rather than a convention enforced by middleware and logs.

Core claim

The central discovery is the split between escaping effects and requested-action traces. A handler may discharge the caller's obligation for an action, but the request event remains in the typed trace and remains visible to policy and audit; handlers cannot erase requests or create commit authority. Static semantics uses spec conformance: type specs, callable specs, and trace specs; trace specs normalize to TraceSpecAlgebra and compile to finite monitors. Typing discharges the abstract trace against the monitor, emits residual checks for dynamic predicates, and the dynamic semantics mediate each request and commit through policy, effect boundary, and monitor. Theorems 5 and 6 state policy sa

What carries the argument

The load-bearing mechanism is the pair (escaping effect row epsilon, requested-action abstraction A) plus the compiled monitor context Pi. Trace specs are normalized to TraceSpecAlgebra atoms (allow set, deny set, before-obligations), compiled to finite monitors, and checked by abstract interpretation over monitor states. The abstract transformer maps abstract events to sets of monitor states; if successor states avoid Bad the transition is proved, if they fall inside Bad the program is rejected, otherwise a residual check is emitted. This three-way discharge is what connects static and dynamic enforcement.

Load-bearing premise

The guarantees depend on the claim that the abstract-interpretation layer over-approximates the concrete monitor transitions; if an abstract event can be judged safe while one of its concrete instances would enter a rejecting state, static discharge could miss a violating trace.

What would settle it

Run a well-typed ETAS program with all residual checks enforced and observe a concrete execution whose trace prefix is rejected by the compiled monitor; or, more directly, exhibit an abstract event eta# and concrete event eta in gamma(eta#) such that the abstract successor set avoids Bad but the concrete transition enters Bad. The prototype and its fixture tests could be used to search for such a case.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Compile-time rejection of missing approvals, forbidden resource access, and ordering violations becomes possible before any model runs.
  • Dry-run, mock, and recovery handlers no longer create audit blind spots: the request is recorded even when the effect does not escape.
  • Anything the compiler cannot prove statically is made explicit as a residual runtime check, so enforcement is never silently dropped.
  • Agent-specific optimizations such as tool-surface specialization, hoisting loop-invariant searches, and parallelizing independent calls can be justified from typed summaries.
  • Audit traces have a uniform typed vocabulary of request, handled, denied, and commit events, supporting replay and checkpointing.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the abstraction soundness gap is closed, the same design could subsume many guardrail layers: policy becomes a compile-time obligation rather than a separate runtime service.
  • The trace-spec calculus may extend naturally to multi-agent delegation, where a parent agent's requested-action abstraction should conservatively include actions requested by subagents.
  • A productive next test is randomized differential checking between the abstract transformer and the concrete monitor to search for over-approximation failures.
  • The distinction between request and commit could be useful beyond agents, for any system needing auditable dry-run side effects.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents ETAS, a language for agent systems with a core calculus (CoreEtas) that separates deterministic computation from agentic nondeterminism and externally visible actions. The static semantics assigns ordinary types, an escaping effect row ε, and a persistent requested-action trace abstraction A to every computation. Trace specs are normalized to TraceSpecAlgebra objects, compiled to finite monitors, and discharged by abstract interpretation; facts that cannot be proved statically are emitted as residual checks R. The dynamic semantics distinguishes request, handled, commit, and denied events, and mediates concrete actions through monitor state and effect boundaries. The paper states preservation, progress, type/effect soundness, handler trace transparency, and policy safety, and reports on a Rust prototype and four case studies.

Significance. If the theorems were established, the paper would offer a valuable integration of row-typed effects, trace automata, handler transparency, and residual static/dynamic enforcement for agent systems. The request/handled/commit/denied event distinction and the principle that handlers do not grant authority are well motivated, and the prototype and case studies give useful evidence of implementability. However, the central static–dynamic bridge is currently incomplete: residual checks are not consumed by any rule of the dynamic semantics, and the soundness of the abstract-interpretation layer is asserted rather than proved. The headline claim that authorization can be reasoned about before and during execution is therefore not yet supported by the formal development as written.

major comments (3)
  1. [§5 (Fig. 11), §6.4 (Thm. 5), §6.2 (Lemma 1)] The residual-check mechanism is absent from the dynamic semantics. The typing judgment emits R = {check(η♯, φ)} (Figs. 5 and 7); §6.1 defines well-formed configurations as 'containing' R; Theorem 5 assumes 'every residual check is enforced before its guarded request or commit event'; and the proof sketch of Lemma 1 says 'residual checks are consumed only after their guarded dynamic test has succeeded.' But none of the rules in Fig. 11 has a premise mentioning R, check(η♯, φ), or the predicate φ. E-Perform-Handle and E-Perform-Commit only consult δ_Π and ε_b; denial rules fire only when δ_Π enters Bad. Thus a residual predicate such as approval freshness or account equality can be false while the monitor state is outside Bad, and the rules still append request/commit events. Theorem 5 and the residCov clause of Theorem 4 are therefore not provable from the stated calculus. The semantics n
  2. [§4.4, §6.4 (Thm. 5 proof sketch)] The soundness of the abstract-interpretation layer is asserted, not proved. The concretization γ_Ξ and abstract transformer Jη♯K^♯_{Ξ,Π} are defined, but no lemma states that γ_Ξ(η♯) is an over-approximation of the represented concrete events, nor that the abstract transformer over-approximates the concrete monitor transition relation. The proof sketch of Theorem 5 says 'soundness of the abstraction ensures...', which assumes exactly the property that needs proof. This is load-bearing because static discharge uses the abstraction to remove runtime checks. A concrete soundness lemma is needed, e.g. for all Q♯ and η♯, {δ_Π(q,η) | q ∈ γ_Π(Q♯), η ∈ γ_Ξ(η♯)} ⊆ γ_Π(Jη♯K^♯_{Ξ,Π}(Q♯)), or the paper must explicitly state this as an unproven assumption rather than presenting it as a consequence of the definitions.
  3. [§6, Theorems 3–6] The central theorems are stated with only proof sketches, and §6 says 'a mechanized proof is future work.' Sketchiness alone need not block publication, but here the gap is not a matter of omitted routine cases: Lemma 1's claim about residual checks has no corresponding rule, and Theorem 5's proof depends on the unproved abstraction soundness. The authors should either provide a complete paper proof of the residual-check evaluation and abstraction soundness, or state clearly in the theorem statements that residual enforcement is an assumption about the runtime rather than a property of the calculus. As written, the theorems give the impression of a stronger guarantee than the formal system actually provides.
minor comments (4)
  1. [Fig. 11] Rule name 'E-Reqest-Deny' is a typo for 'E-Request-Deny'.
  2. [§3.1 vs §5] The metavariable τ is used both for types (Fig. 4) and for trace prefixes (⟨e, H, τ⟩ in Fig. 11). This is a real notational clash; consider renaming the trace prefix, e.g. tr or h.
  3. [§4.4] The abstract domain D♯_Π = P(Q_Π) and γ_Ξ are defined abstractly, but no concrete example is given. A short illustration for the ApprovalBefore spec showing how a residual check like account equality arises would greatly improve clarity.
  4. [§8] The RQ answers are supported by four compact case-study snippets rather than a systematic benchmark or error-injection study. That is acceptable for an artifact-oriented evaluation, but the wording in the abstract and conclusion should avoid implying a broader evaluation than the evidence supports.

Circularity Check

0 steps flagged

No circularity: Theorems 3-6 are conventional metatheoretic properties of the paper's own static and dynamic semantics; there are no fitted predictions, no load-bearing self-citations, no imported uniqueness, and no ansatz smuggled via citation. The residual-check enforcement gap is a proof-formalization concern, not a circular reduction.

full rationale

I tracked the claimed derivation chain: the static semantics (Figures 4-10) derives types, effect rows, requested-trace abstractions, and residual checks from declared signatures and compiled monitors; the dynamic semantics (Figure 11) appends request/handled/commit/denied events only when monitor and boundary premises succeed; Theorems 3-6 are stated as properties of these definitions, with proof sketches that appeal to the rules themselves. I could not exhibit any equation-level reduction of a conclusion to an input. There are no fitted constants or parameters, no quantity is fit to a subset and then 'predicted' as validation, no author self-citations are load-bearing (the cited effect/handler/automata literature is external and canonical), no uniqueness theorem is imported from the authors' prior work, and no ansatz is smuggled in by citation. The closest concern is in Section 4.4/Section 6.4: Theorem 5 supposes 'every residual check is enforced before its guarded request or commit event,' while the small-step rules in Figure 11 never consume check(eta#, phi), and the proof sketch's statement that 'soundness of the abstraction ensures' all concrete events keep the monitor outside Bad is asserted rather than proved; Section 6 explicitly says 'a mechanized proof is future work.' This is a substantive omission in the formal argument -- the policy-safety theorem may not be derivable from the stated calculus alone -- but it is a soundness/proof gap, not a circular derivation: the conclusion is not by construction identical to the hypothesis, and the paper itself flags the missing mechanized proof. Similarly, the RQ4 answer that the recorded information 'will enable an optimizer' and the author-authored case studies are weak external-validation evidence, not circularity in the formal derivation. I therefore find no significant circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

The system introduces no numeric free parameters and no empirical entities; its formal constructs (requested-action trace abstractions, residual obligations) are the content of the design. The load-bearing assumptions are the soundness of the abstract-interpretation layer, the exhaustiveness of action mediation at runtime, the enforcement of residual checks by the interpreter, and the fidelity of action matching.

axioms (4)
  • ad hoc to paper The abstract requested-trace analysis over monitor states is a sound over-approximation: the concretization γ_Ξ covers every concrete event represented by an abstract event, and the abstract transformer Jη^♯K^♯ over-approximates the concrete monitor transition relation.
    Invoked in §4.4 and relied on in the proof sketch of Theorem 5 ('soundness of the abstraction ensures...'); no proof or mechanization is supplied, and it is load-bearing for policy safety.
  • domain assumption Every concrete external operation is mediated by the core request/commit machinery; no model output or host service can perform an unmediated host operation.
    Stated in §5.2 ('no model output can cause an unmediated host operation'); this is an architectural assumption about the deployment and sandbox, not proven by the calculus.
  • domain assumption Well-formed configurations include all residual checks R emitted by typing, and the interpreter/runtime enforces each residual check before the guarded request or commit event.
    Used to state Theorem 3 and Theorem 5 (§6.1, §6.4). If a runtime omits or mis-orders residual checks, the policy-safety guarantee does not transfer to implementations.
  • domain assumption Action matching between concrete actions and abstract patterns, including spec-bound resource predicates, is faithful and decidable via type-spec witnesses in Ξ.
    Underlies effect-row subsumption, monitor matching and concretization in §§4.2–4.4; the paper sketches evidence-indexed matching but does not prove completeness or decidability.

pith-pipeline@v1.3.0-alltime-deepseek · 24543 in / 14025 out tokens · 159880 ms · 2026-08-01T17:03:23.700124+00:00 · methodology

0 comments
read the original 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.

Figures

Figures reproduced from arXiv: 2607.17780 by Huiri Tan, Jiasi Shen, Puyang Zhang, Shangyu Li, Yikun Wang.

Figure 1
Figure 1. Figure 1: Draft-approve-publish workflow in framework code and [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. 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. values from ProjectMemory.Sec… view at source ↗
Figure 3
Figure 3. 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. fully general algebraic effects [15, 20, 27]. The goal is not to make all control effects programmable. The goal is to let tests, re… view at source ↗
Figure 4
Figure 4. Figure 4: Static ingredients of Core Etas: metavariables, value and handler types, schemes, and typing envi￾ronments. 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. may request even if a handler interprets them locally. The conformance artifac… view at source ↗
Figure 5
Figure 5. Figure 5: Core bidirectional typing with spec conformance. Each derivation returns a value type, escaping [PITH_FULL_IMAGE:figures/full_fig_p011_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Typing first-class handlers and handle-with expressions. T-HandleWith removes handled effects from the escaping row while preserving requests in 𝐴; 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. trace abstractions 𝐴 ::= ∅ | 𝜂 ♯ | 𝐴1 ; 𝐴2 | 𝐴1 ⊔ 𝐴2 | 𝐴 ★ abstract events … view at source ↗
Figure 7
Figure 7. Figure 7: Static requested-action traces and residual obligations. Trace abstractions sequence, join, and iterate [PITH_FULL_IMAGE:figures/full_fig_p012_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Terminating compile-time spec calculus. The figure defines kinds, action patterns, callable shapes, [PITH_FULL_IMAGE:figures/full_fig_p014_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Kind-directed conformance from normalized specs to static checking. Type specs resolve witnesses, [PITH_FULL_IMAGE:figures/full_fig_p014_9.png] view at source ↗
Figure 10
Figure 10. 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 𝑝 ≫ 𝑞 requires prior matching 𝑝 events. commit. The active environment Π denotes their product 𝑀Π; any rejecting … view at source ↗
Figure 11
Figure 11. Figure 11: Call-by-value dynamic semantics over ⟨𝑒, 𝐻, 𝜏⟩. 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 distinct… view at source ↗
Figure 12
Figure 12. Figure 12: Four language-visible agent-engineering cases. The left column stacks context engineering (a), which [PITH_FULL_IMAGE:figures/full_fig_p024_12.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

30 extracted references · 3 canonical work pages

  1. [1]

    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

    doi:10.1145/3729296 2025

  2. [2]

    Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers.Journal of Logical and Algebraic Methods in Programming84, 1 (Jan. 2015), 108–123. doi:10.1016/j.jlamp.2014.02.001

    doi:10.1016/j.jlamp.2014.02.001 2015

  3. [3]

    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

    work page doi:10.1145/3290319 2019

  4. [4]

    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

    doi:10.1145/3527320 2022

  5. [5]

    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

    doi:10.1145/3656401 2024

  6. [6]

    CloudWeGo. 2026. Eino User Manual. https://www.cloudwego.io/docs/eino/ Accessed: 2026-06-17

    2026

  7. [7]

    Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InProceedings 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–...

    arXiv 1977

  8. [8]

    CrewAI. 2026. CrewAI Documentation. https://docs.crewai.com/ Accessed: 2026-06-17

    2026

  9. [9]

    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

    work page doi:10.1145/3656447 2024

  10. [10]

    Dorothy E. Denning. 1976. A lattice model of secure information flow.Commun. ACM19, 5 (May 1976), 236–243. doi:10.1145/360051.360056

    arXiv 1976

  11. [11]

    Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. 2024. Choral: Object-oriented Choreographic Program- ming.ACM Trans. Program. Lang. Syst.46, 1, Article 1 (Jan. 2024), 59 pages. doi:10.1145/3632398

    doi:10.1145/3632398 2024

  12. [12]

    Griffiths

    Brent D. Griffiths. 2026. Forget prompt engineering: ‘Loop engineering’ is all the rage now. https://www.businessinsider. com/what-are-loops-ai-engineering-tips-2026-6 Accessed: 2026-07-03

    2026

  13. [13]

    Daniel Hillerström and Sam Lindley. 2016. Liberating effects with rows and handlers. InProceedings 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

    arXiv 2016

  14. [14]

    Vasconcelos, and Makoto Kubo

    Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. InProgramming Languages and Systems, Chris Hankin (Ed.). Springer Berlin Etas 27 Heidelberg, Berlin, Heidelberg, 122–138

    1998

  15. [15]

    Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action. InProceedings of the 18th ACM SIGPLAN In- ternational Conference on Functional Programming(Boston, Massachusetts, USA)(ICFP ’13). Association for Computing Machinery, New York, NY, USA, 145–158. doi:10.1145/2500365.2500590

    arXiv 2013

  16. [16]

    Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, and Tachio Terauchi. 2024. Answer Refinement Modification: Refine- ment Type System for Algebraic Effects and Handlers.Proceedings of the ACM on Programming Languages8, POPL, Article 5 (2024), 33 pages. doi:10.1145/3633280

    work page doi:10.1145/3633280 2024

  17. [17]

    LangChain. 2026. LangGraph Overview. https://docs.langchain.com/oss/python/langgraph/overview Accessed: 2026-06-17

    2026

  18. [18]

    Daan Leijen. 2014. Koka: Programming with Row Polymorphic Effect Types.Electronic Proceedings in Theoretical Computer Science153 (June 2014), 100–126. doi:10.4204/eptcs.153.8

    doi:10.4204/eptcs.153.8 2014

  19. [20]

    Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. InProceedings 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

    arXiv 2017

  20. [21]

    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

    Pith/arXiv arXiv 2025

  21. [22]

    Microsoft. 2026. Agent Framework Documentation. https://learn.microsoft.com/en-us/agent-framework/ Accessed: 2026-06-17

    2026

  22. [23]

    Microsoft. 2026. AutoGen Documentation. https://microsoft.github.io/autogen/stable/ Accessed: 2026-06-17

    2026

  23. [24]

    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

    arXiv 2026

  24. [25]

    OpenAI. 2026. OpenAI Agents SDK Documentation. https://openai.github.io/openai-agents-python/ Accessed: 2026-06-17

    2026

  25. [26]

    Gordon Plotkin and John Power. 2003. Algebraic Operations and Generic Effects.Applied Categorical Structures11, 1 (2003), 69–94. doi:10.1023/A:1023064908962

    doi:10.1023/a:1023064908962 2003

  26. [27]

    Gordon D Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects.Logical Methods in Computer Science9, 4, Article 23 (Dec. 2013), 36 pages. doi:10.2168/lmcs-9(4:23)2013

    doi:10.2168/lmcs-9(4:23)2013 2013

  27. [28]

    Schneider

    Fred B. Schneider. 2000. Enforceable security policies.ACM Trans. Inf. Syst. Secur.3, 1 (Feb. 2000), 30–50. doi:10.1145/ 353323.353382

    arXiv 2000

  28. [29]

    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

    Pith/arXiv arXiv 2026

  29. [30]

    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

    doi:10.1145/3563289 2022

  30. [31]

    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

    Pith/arXiv arXiv 2026