λ_A: First Formal Type System for LLM Agent Composition Proves Safety and Termination
arXiv·high signal
Researchers present λ_A, a typed lambda calculus for agent composition that extends simply-typed lambda calculus with oracle calls, bounded fixpoints (the ReAct loop), probabilistic choice, and mutable environments. The paper proves type safety, termination of bounded fixpoints, and soundness of derived lint rules, with partial Coq mechanization (1,560 lines). This gives agent framework builders the first principled way to determine whether an agent configuration is well-formed or will terminate — a missing piece in every existing framework.