$\lambda_A$: A Typed Lambda Calculus for LLM Agent Composition

TL;DR

This paper introduces $ extbackslash lambda_A$, a formal typed lambda calculus for LLM agent composition, enabling rigorous analysis, error detection, and unification of various agent paradigms.

Contribution

It extends the simply-typed lambda calculus with features for agent modeling, proves key properties, and demonstrates practical tools and insights for real-world agent configurations.

Findings

94.1% of real-world GitHub agent configs are structurally incomplete under $ extbackslash lambda_A$

YAML-only lint precision is 54%, rising to 96-100% with combined YAML and Python AST analysis

Five mainstream agent paradigms embed as fragments of $ extbackslash lambda_A$

Abstract

Existing LLM agent frameworks lack formal semantics: there is no principled way to determine whether an agent configuration is well-formed or will terminate. We present $\lambda_A$, a typed lambda calculus for agent composition that extends the simply-typed lambda calculus with oracle calls, bounded fixpoints (the ReAct loop), probabilistic choice, and mutable environments. We prove type safety, termination of bounded fixpoints, and soundness of derived lint rules, with full Coq mechanization (1,519 lines, 42 theorems, 0 Admitted). As a practical application, we derive a lint tool that detects structural configuration errors directly from the operational semantics. An evaluation on 835 real-world GitHub agent configurations shows that 94.1% are structurally incomplete under $\lambda_A$, with YAML-only lint precision at 54%, rising to 96--100% under joint YAML+Python AST analysis on 175 samples. This gap quantifies, for the first time, the degree of semantic entanglement between declarative configuration and imperative code in the agent ecosystem. We further show that five mainstream paradigms (LangGraph, CrewAI, AutoGen, OpenAI SDK, Dify) embed as typed $\lambda_A$ fragments, establishing $\lambda_A$ as a unifying calculus for LLM agent composition.