$λ_A$: A Typed Lambda Calculus for LLM Agent Composition

Qin Liu

cs.PLApr 13, 2026

$λ_A$ : A Typed Lambda Calculus for LLM Agent Composition

Authors: Qin Liu

Organizations: State Key Laboratory of Novel Software Technology, Nanjing University, Nanjing, Jiangsu, China · Software Institute, Nanjing University, Nanjing, Jiangsu, China

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 $λ_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 $λ_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 $λ_A$ fragments, establishing $λ_A$ as a unifying calculus for LLM agent composition.

Figures & tables

Layer	Formalism	LoC	Key Classes
Core DSL	$\lambda_{\!A}$ syntax (Def. 3.1 )	575	13 classes: Term, Lam, Compose, Loop, Tool, Route, etc.
from_config	Compilation (§ 5.3 )	999	Compiler, 5 type branches
Runtime	Op. semantics (§ 4 )	2,097	Executor, ReActEngine, ActionParser
CLI + lint	Static analysis (§ 5 )	1,232	8 commands, 26 lint rules
Total		4,903	58 classes

Table 1. Implementation architecture: code

\leftrightarrow

formalism correspondence.

Rule	Level	Count	Pct	Lambda Semantics
mcp.localTools	ERROR	483	57.8%	No $\lambda x.x$ base case
systemPrompt	ERROR	282	33.8%	$\lambda x.\bot$ (undefined body)
model	ERROR	51	6.1%	No LLM $=$ no computation
react.maxSteps	ERROR	1	0.1%	$Y$ unbounded
Total configs with $\geq$ 1 ERROR		786	94.1%
Clean (no ERROR/WARN)		46	5.5%

Table 2. Lint results on 835 GitHub agent configurations.

Framework	Configs	w/ ERROR	Dominant Defect	Nature
CrewAI	441	$\sim$ 430	mcp.localTools	structural $\dagger$
Generic	283	$\sim$ 260	systemPrompt	genuine
Multi-agent	45	$\sim$ 40	systemPrompt	genuine
LangChain	35	$\sim$ 30	systemPrompt	genuine
AutoGen	22	$\sim$ 20	model	genuine
lambdagent	9	$\sim$ 6	mixed	genuine

Table 3. Lint results stratified by framework.

Tool	Domain	Precision	Source
FindBugs	Java bugs	42–53%	Ayewah et al., 2008
SpotBugs	Java bugs	$\sim$ 50%	FindBugs successor
Pylint (all rules)	Python style/bugs	55–65%	Community reports
ESLint (recommended)	JavaScript	60–70%	Varies by config
Infer	C/Java memory	65–80%	Calcagno et al., 2015
lambdagent lint (YAML)	Agent config	54%	This paper

Table 4. Precision of static analysis tools across domains.

Metric	50-sample		175-sample
	YAML	+Python	YAML	+Python
True Positive	27	27	90	89
False Positive	23	1	85	0
Downgraded to Info	—	22	—	86
Precision	54%	96%	51%	100%
95% CI (Wilson)	[40,67]	[82,99]	[44,59]	[96,100]

Table 5. YAML-only vs. joint YAML+Python analysis.

Operation	Latency	Relative to LLM call
Tool call	2.0 $\mu$ s	0.0001%
Compose (3 stages)	4.9 $\mu$ s	0.0002%
If branch	4.6 $\mu$ s	0.0002%
Pair	3.4 $\mu$ s	0.0002%
Loop (5 steps)	11.2 $\mu$ s	0.0006%
Memory (3 keys)	2.4 $\mu$ s	0.0001%

Table 6. DSL wrapper overhead (excluding LLM latency).

Pattern	$\lambda_{\!A}$ Constructs	Output	Pass
LLM call	lam	“Paris”	✓
3-stage pipe	>> , $3{\times}$ lam	translate $\to$ fmt	✓
ReAct loop	$\textbf{fix}_{3}$ , case	“105”	✓
Guard+retry	guard	3 words	✓
Parallel	$\langle\textbf{lam}_{1},\textbf{lam}_{2}\rangle$	sum+kw	✓
Router	case , $3{\times}$ lam	“ $2x$ ”	✓

Table 7. Real-world agent pattern tests. Each pattern constructs a production-style

\lambda_{\!A}

term, executes via real LLM calls, and verifies the output matches the operational semantics prediction. “Output” shows the actual LLM result.

Agent	$n$	Predicted max	Actual	Tightness
Church factorial (3!)	4	4 calls	4	1.0 $\times$
Church factorial (5!)	6	6 calls	6	1.0 $\times$
ReAct research (ex02)	20	40 calls	15	2.7 $\times$
Self-learning (demo4)	10	20 calls	8	2.5 $\times$
Refine loop (demo1)	5	10 calls	3	3.3 $\times$

Table 8. Cost Bound validation: predicted vs. actual oracle calls.

Paradigm	Core Pattern	$\lambda_{\!A}$ Fragment	Configs
Graph (LangGraph)	Cond. edges, cycles	case + $\textbf{fix}_{n}$ + >>	35
Role-driven (CrewAI)	Role dispatch, handoff	case + >>	441
SDK wrapper (OpenAI)	LLM call + tools	lam + tool	283
Multi-agent (AutoGen)	Group chat, turns	$\textbf{fix}_{n}$ + case	22
Low-code (Dify)	YAML pipeline	from_config	54

Table 9. Five agent architecture paradigms as

\lambda_{\!A}

fragments. Each paradigm uses only a subset of the 11 term formers. “Configs” indicates the number of real-world GitHub configurations from our dataset (Section 7 ) that exercise each paradigm’s translation.

	$\lambda_{\!A}$	DSPy	Agint	CSP/ $\pi$	Agentic 2.0
Formal syntax	✓	—	✓	✓	✓
Type system	✓	—	✓	—	✓
Type safety proof	Coq	—	—	—	—
Termination	$\textbf{fix}_{n}$	—	—	—	—
Static analysis	26 rules	—	—	—	—
Empirical (configs)	835	—	—	—	—

Table 10. Comparison of agent/workflow formalisms.

LLM Agents

Large language model agents use language models to plan, use tools, and act across multi-step tasks and environments.

See all 705 papers

Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment
May 18, 2026S. Bensalem, Y. Dong, M. Franzle +6AI Agent Reliability LLM Guardrails
1CSX-AI, France · University of Liverpool, UK · 3Carl von Ossietzky Universität Oldenburg, Germany +2
The LLMbda Calculus: AI Agents, Conversations, and Information Flow
Feb 23, 2026Zac Garby, Andrew D. Gordon, David SandsPrompt Injection Attacks on AI Agents LLM Agent Harnesses
University of Nottingham, Nottingham, UK · University of Edinburgh, Edinburgh, UK · Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweden
LLM-as-Code: Agentic Programming for Agent Harness
Jun 14, 2026Junjia Qi, Zichuan Fu, Jingtong Gao +4AI Agent Reliability LLM Agent Orchestration
City University of Hong Kong · Tencent Jarvis Lab

May 18, 2026J/K move · Enter open · S save

Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment

S. Bensalem, Y. Dong, M. Franzle, X. Huang+5

1CSX-AI, France · University of Liverpool, UK · 3Carl von Ossietzky Universität Oldenburg, Germany+2

AI Agent Reliability LLM Guardrails Runtime Enforcement for AI Agents LLM Agent Safety

Open paper AskPDF arXiv

This position paper argues that enforcing LLM agent safety within a single abstraction layer is not merely suboptimal but categorically insufficient for deployed LLM agents -- a structural consequence of how agent execution works, not a contingent limitation of current systems. The three dimensions that jointly constitute safe operation -- semantic intent and policy compliance, environmental validity, and dynamical feasibility -- each depend on a strictly distinct set of information that becomes available at different stages of execution. No single guardrail can certify all three. We argue that the community must respond with a contract-based architecture in which each safety dimension is enforced by an independently certified layer whose probabilistic guarantee satisfies the next layer's assumption. We sketch such an architecture and derive the compositional system-level safety bounds it admits via the chain rule of probability. Three open problems stand between this and a deployable standard: bound estimation from non-i.i.d.\ traces, graceful degradation of contracts under deployment drift, and extension to multi-agent settings -- the most important unfinished business in LLM agent runtime assurance.

Abstract

LLM Agents

Explore similar work

Position: A Three-Layer Probabilistic Assume-Guarantee Architecture Is Structurally Required for Safe LLM Agent Deployment

The LLMbda Calculus: AI Agents, Conversations, and Information Flow

LLM-as-Code: Agentic Programming for Agent Harness