Pith. sign in

REVIEW 4 major objections 5 minor 6 cited by

A lambda calculus with labelled conversations makes prompt-injection defence provably sound.

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-02 21:24 UTC pith:NUH5RVGL

load-bearing objection The calculus is the contribution; the abstract is the liability. the 4 major comments →

arxiv 2602.20064 v2 pith:NUH5RVGL submitted 2026-02-23 cs.PL cs.AIcs.CR

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

Zac Garby , Andrew D. Gordon , David Sands This is my paper
classification cs.PL cs.AIcs.CR MSC 68N1868Q6068M25
keywords prompt injectioninformation flow controllambda calculusnoninterferenceAI agentsconversationsdynamic labelsLLMbda
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.

The paper tries to establish that the core of agentic LLM programming—prompt-response conversations, forking, clearing, and code generation—can be captured in a small untyped lambda calculus with dynamic information-flow labels, and that this calculus satisfies a formal noninterference theorem. That would matter because today's strongest prompt-injection defences rely on provenance and separation of duty but lack a rigorous semantic foundation; here, isolation becomes ordinary program structure and reclassification becomes an auditable construct. The central result, Theorem 1, proves termination-insensitive noninterference for three classes of programs, the most usable of which replaces unrestricted label tests with assertion and strong-test primitives that still allow policy checks. On a banking benchmark, an agent built in the calculus with enforcement always on matches the utility of a leading dual-LLM defence and resists all but two of 1296 attacked runs.

Core claim

LLMbda is an untyped call-by-value lambda calculus whose semantics carries a program-counter label and a labelled conversation history, and adds three agentic primitives: @e asks the LLM a prompt and parses the response, forke runs an expression against a copy of the conversation and discards it, and clear resets the conversation. Every value carries a security label that every reduction propagates, and the semantics enforces a no-high-upgrade discipline on the conversation state. Theorem 1 shows that termination-insensitive noninterference holds for (1) expressions without label tests, (2) expressions using only one non-bottom label, and (3) expressions where tests appear only as assertions

What carries the argument

The load-bearing mechanism is the labelled conversation: a big-step semantics with judgements pc ⊢ C, e ⇓ C′, V where pc is the program-counter label and C the labelled history. The @ rule serialises the erased value of e, appends it to the conversation, and parses the model's deterministic response; the erase function strips subterms labelled above the permitted level, and the no-high-upgrade constraint prevents a low conversation from being upgraded from a high context. The n-indistinguishability relation ∼_n and the erasure lemma (v ∼_n v′ implies erase_n(v) = erase_n(v′)) are the proof machinery that carries the noninterference argument. The derived primitives assert_k e and k?? e replac

Load-bearing premise

The noninterference proof assumes, without stating it as a semantic condition, that serialise(erase_n(v)) hides every label difference between n-indistinguishable values; if the prompt serialiser leaks such differences, the theorem's PROMPT case—and with it the whole guarantee—no longer goes through.

What would settle it

Feed two values that are indistinguishable at level k but differ only in subterms labelled above k through the interpreter's serialise path and compare the resulting prompts; if the prompts are not identical, Theorem 1 fails. A simpler end-to-end check: run a qualifying program twice with only a {U}-labelled input changed and look for any observable difference in a {S}-labelled output or conversation.

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

If this is right

  • Any agent programme written in the calculus inherits the noninterference guarantee, so label-checking wrappers (like a send-email policy that requires trusted subject and body) enforce the intended security policy rather than just hoping the model complies.
  • The dual-LLM separation pattern becomes a library-level construction—a privileged planner generates code, a quarantined conversation processes untrusted data—and remains covered by the same theorem.
  • The three sublanguages map a design space: drop label tests, keep a single non-bottom label, or use assertion/strong-test primitives; each is provably safe, so implementations can choose a point on the spectrum.
  • Because the guarantee is termination-insensitive, the defence blocks data-flow leaks but explicitly permits leaks through termination (e.g., a blocked prompt), which is the same trade-off as classical dynamic information-flow control.
  • The benchmark result indicates the formal calculus is not just theoretical: with enforcement always on, an LLMbda agent keeps utility on a banking agent task while resisting all but two of 1296 attacks.

Where Pith is reading between the lines

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

  • If probabilistic model behaviour were admitted, the theorem would likely need a probabilistic analogue of noninterference; the paper points this out, but a concrete probabilistic version would make the guarantee match real nondeterministic sampling.
  • A practical engineering rule follows from the proof's PROMPT case: the serialiser must be tested for accidental label leakage, since erased values with different hidden labels must serialise to identical prompts.
  • The conversation-as-state view suggests a generalisation to multi-agent systems where each subagent keeps its own labelled history, with fork/clear as the composition operators between them.
  • One could imagine a static type system or linter that rejects label tests outside the assert/strong-test forms, turning Theorem 1's third sublanguage into an enforceable programming discipline.

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

4 major / 5 minor

Summary. The paper introduces LLMbda, an untyped call-by-value lambda calculus with dynamic information-flow control and primitives for LLM conversation management (@, fork, clear). It provides a big-step operational semantics with label propagation, a deterministic abstraction of LLM generation via serialise/parse/generate functions, and states a termination-insensitive noninterference (TINI) theorem restricted to three sublanguages: expressions without label tests, expressions using only one non-bottom label, and expressions where tests occur only via assert or strong tests. The paper also describes a Python interpreter and illustrates the calculus on postcode extraction, repair loops, a tool-calling agent, and a CaMeL-style code-generation defence. The abstract, however, claims a probabilistic noninterference theorem over the whole calculus, a machine-checked Lean proof, and a specific AgentDojo benchmark result, none of which is supported by the body of the paper.

Significance. The core idea of modelling LLM-agent conversations as first-class constructs in a lambda calculus with information-flow labels is timely and potentially valuable. The big-step semantics is written with care, and the explicit identification of a counterexample showing that unrestricted label testing breaks TINI is an honest and useful contribution. The restricted TINI statements, if fully proved, would be a meaningful formal foundation for provenance-based prompt-injection defences. However, the paper's headline claims — whole-calculus probabilistic noninterference, Lean-verified proofs, and a concrete AgentDojo result — are not established by the submitted manuscript. The appendix proof of the main theorem contains load-bearing gaps, and no machine-checked artifacts are provided. The significance of the work as presented is therefore substantially lower than advertised.

major comments (4)
  1. [Abstract; Section IV; Section III-D; Section I.H] The abstract states a 'termination-insensitive probabilistic noninterference theorem over the whole calculus' and claims all proofs are in Lean. The body proves only a deterministic TINI for three restricted sublanguages (Theorem 1). Section IV explicitly presents a counterexample (M:true vs M:(H:false)) showing the full calculus does not satisfy TINI, and Section III-D assumes a deterministic generation function J·K; Section I.H lists probabilistic semantics as future work. The abstract's unrestricted probabilistic claim is therefore false for the submitted semantics, and the Lean-verification claim is unsupported because no Lean artifacts appear anywhere in the manuscript.
  2. [Appendix A, PROMPT case; Lemma 2] The proof of Theorem 1 is incomplete in a load-bearing way. In the PROMPT case, the argument requires that if n_i ⊑ k and v_0 ∼_k v_1 then serialise(erase_{n_i}(v_0)) = serialise(erase_{n_i}(v_1)); the text invokes an unstated 'serialisation assumption'. This property is not included in the semantics, in Definition 1, or in the statement of Theorem 1. If serialise formats labelled subterms differently, the conclusion fails. Lemma 2, the central erasure property that v ∼_n v' implies erase_n(v)=erase_n(v'), is also stated without proof and is needed for the erasure-based reasoning. These omissions mean the main theorem is not actually proved as written; the gaps could be repaired by adding explicit axioms and completing the induction, but they are not merely cosmetic.
  3. [Abstract; Section V] The abstract claims 'Our harness and all proofs are in Lean' and describes 'the first LLM agent harness whose executable is the subject of machine-checked security theorems'. The implementation described in Section V is a Python interpreter (approximately 4000 lines) using the OpenAI Responses API, with no mention of Lean, no proof scripts, and no repository link. The machine-checked verification claim is thus unsupported by the submission. If the Lean formalisation exists, it needs to be provided or at least cited with a clear artifact identifier; without it, the central advertised contribution cannot be assessed.
  4. [Abstract (AgentDojo claim)] The abstract reports a specific empirical result: 'an agent built within LLMbda, enforcement always on, matches the utility of CaMeL ... and resists all but two of 1296 attacked runs'. The body contains no benchmark section, no experimental setup, no baseline definition, no hyperparameter details, and no presentation of these 1296 runs. This empirical claim is therefore unverifiable from the manuscript as submitted and should either be removed or supported by a proper evaluation section.
minor comments (5)
  1. [Appendix A, ASSERT case] The ASSERT case of the proof is sketched more briefly than the rest. In particular, the treatment of the divergent else-branch Ω and the role of termination-insensitivity should be made explicit. As written, 'since both computations return the same labelled value' glosses over the case analysis needed when one side of the assert diverges.
  2. [Section IV, Lemma 3] Lemma 3 says the derived rules for assert and strong test are 'sound and complete'. Completeness is not defined in the paper; it would be helpful to state the intended notion (e.g., derivability equivalence with the encoding) to avoid confusion.
  3. [Section VI.B] There is a typographical inconsistency: 'Willitson' appears where 'Willison' is intended (the same author is correctly spelled elsewhere, e.g., references [8], [11]).
  4. [Section III-D] The definition of erase_n is given by equations but the paper does not specify an ordering or pattern-matching convention for the rules; for example, the second equation could overlap with the first if fork expressions could be labelled. It would be clearer to state that erasure is defined by recursion on the expression structure and that labels intercept at the top level.
  5. [Throughout] The paper would benefit from a short table of the labels used in the proof (pc, k, n, l, m) and their roles; the appendix proof uses several labels that can be hard to track, especially in the PROMPT and STRONGTEST cases.

Circularity Check

0 steps flagged

No material circularity; the central TINI theorem is derived from the semantics, though the abstract overclaims probabilistic and Lean-verified guarantees.

full rationale

The central derivation is self-contained rather than circular. Theorem 1 (Sec. IV) is proved in Appendix A by induction over the big-step semantics; the three sublanguage restrictions are explicit hypotheses, and the Sec. IV counterexample (M:true vs M:(H:false)) shows that without them the property genuinely fails, so the restrictions are not hiding the conclusion in the definitions. The ~_k/erase machinery does real work: Lemma 2 is a consequence of the inductive definitions, although the appendix omits its proof. In the (PROMPT) case, the phrase 'By the serialisation assumption' is terse, but once erasure equality is established, p0=p1 follows from serialise being a function; this is not an assumed form of the theorem's conclusion. No fitted parameter is renamed as a prediction, and no load-bearing uniqueness claim or ansatz is imported through self-citation. The self-citations that appear, e.g. [21] and [28], concern standard definitions or future-work context and are not load-bearing for Theorem 1. The serious problems are overclaim and verification gaps, not circularity: the abstract promises a 'probabilistic noninterference theorem over the whole calculus' and 'all proofs are in Lean', while Sec. I.H states that LLM determinism is an assumption and probabilistic semantics is left to future work, Sec. IV restricts Theorem 1 to three sublanguages, and Appendix A contains an unproved Lemma 2 and an unstated serialisation step, with no Lean artifacts supplied. These are correctness and completeness concerns and should be weighed as such, but they do not make the derivation circular.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 3 invented entities

The calculus itself is the contribution; the only truly postulated entities are the three conversation-control primitives, which have clear semantics and interpreter support. The main unstated load-bearing assumptions are the determinism and erasure-respecting behaviour of the semantic functions serialise, parse, and the model generator J·K; these are used in the proof but not flagged as axioms in the theorem statement.

axioms (4)
  • domain assumption The underlying LLM generator J·K is deterministic: r = J·K(p).
    Section III-D: 'make the simplifying assumption that it is deterministic'. The theorem is proved for this assumption; probabilistic behaviour is deferred to future work (Section I-H).
  • ad hoc to paper Serialise is deterministic and respects erasure: v0 ∼_k v1 with n_i ⊑ k implies serialise(erase_k(v0)) = serialise(erase_k(v1)).
    Used in the PROMPT case of the Theorem 1 proof (Appendix A), but never stated as a semantic axiom or pre-condition of the theorem in Section III or IV.
  • ad hoc to paper Parse produces label-free closed expressions and respects the sublanguage restrictions.
    Section IV: 'we implicitly assume that the parse function, in addition to producing label-free closed expressions, respects the same constraints.' The parse function is otherwise unspecified.
  • ad hoc to paper Central erasure property: if two labelled values are n-indistinguishable, their n-erasures are equal.
    Section III-D states this as a 'central erasure property (formalised later)', but the appendix does not include a proof; the TINI proof relies on it.
invented entities (3)
  • @ (LLM generation primitive) independent evidence
    purpose: Invoke an LLM within an expression, extending the conversation and parsing the response as a value.
    Its behaviour is grounded in an interpreter and running examples (Section VI); the TINI theorem makes falsifiable predictions about its information flow.
  • fork (conversation fork) independent evidence
    purpose: Save and restore the current conversation around evaluation of a sub-expression.
    Well-defined by the big-step semantics; interpreter demonstrations provide evidence. Not an unexplained entity.
  • clear (conversation clear) independent evidence
    purpose: Reset the current conversation to empty, quarantining from past history.
    Used in the CaMeL-style examples; semantics is explicit and testable.

pith-pipeline@v1.3.0-alltime-deepseek · 26545 in / 15256 out tokens · 138319 ms · 2026-08-02T21:24:28.537687+00:00 · methodology

0 comments
read the original abstract

Large language models are increasingly deployed as agents: they plan, call tools, read untrusted data, and act on the results. This exposes them to prompt injection: data meant only to be read is obeyed as an instruction. The most principled defences replace content inspection with provenance: classifying data by source and keeping trusted and untrusted apart through a separation of duty (the dual-LLM pattern) and information-flow control. Yet the leading systems are hard to fully trust: flow tracking is easy to get wrong, deliberate relaxations are hard to audit, and the dual-LLM pattern is hard-wired into the architecture. We present LLMbda, an untyped call-by-value lambda calculus that makes provenance-based defence both expressible and provably sound, without committing to an architecture. It adds the operational core of agentic systems as first-class constructs: prompt-response conversations that can be forked and cleared, code generation, and dynamic information-flow control in which every value carries a label that every reduction propagates. Isolation becomes a policy a program expresses, and reclassification an explicit, auditable construct. Our central result is a termination-insensitive probabilistic noninterference theorem over the whole calculus, including code-generating agents, with an insulated variant that holds even when the attacker chooses all untrusted inputs. The verified interpreter is itself the harness that calls the model, to our knowledge the first LLM agent harness whose executable is the subject of machine-checked security theorems, so every agent inherits the guarantee. On the AgentDojo banking benchmark, an agent built within LLMbda, enforcement always on, matches the utility of CaMeL, a leading dual-LLM defence, run without its policy checks (which halve its utility), and resists all but two of 1296 attacked runs. Our harness and all proofs are in Lean.

Figures

Figures reproduced from arXiv: 2602.20064 by Andrew D. Gordon, David Sands, Zac Garby.

Figure 1
Figure 1. Figure 1: Imperative programming in the monadic style. [PITH_FULL_IMAGE:figures/full_fig_p020_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Tool-calling agent for Fig 5 of the CaMeL paper [ [PITH_FULL_IMAGE:figures/full_fig_p021_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Direct code generation 22 [PITH_FULL_IMAGE:figures/full_fig_p022_3.png] view at source ↗

discussion (0)

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

Forward citations

Cited by 6 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. ChainCaps: Composition-Safe Tool-Using Agents via Monotonic Capability Attenuation

    cs.CR 2026-05 unverdicted novelty 6.0

    ChainCaps prevents permission laundering in tool-using agents by enforcing monotonic capability attenuation through budget intersection, reducing attack success from 25-68% to 0-4.8% on 82 tasks while maintaining 96-1...

  2. ChainCaps: Composition-Safe Tool-Using Agents via Monotonic Capability Attenuation

    cs.CR 2026-05 unverdicted novelty 6.0

    ChainCaps implements monotonic capability attenuation via budget intersection in a transparent MCP proxy, cutting attack success from 25-68% to 0-4.8% on 82 tasks while keeping benign completion at 96-100%.

  3. ChainCaps: Composition-Safe Tool-Using Agents via Monotonic Capability Attenuation

    cs.CR 2026-05 unverdicted novelty 5.0

    ChainCaps blocks permission laundering in agent tool chains by monotonic capability attenuation via budget intersection, cutting attack success from 25-68% to 0-4.8% on 82 tasks while keeping 96-100% benign performance.

  4. ChainCaps: Composition-Safe Tool-Using Agents via Monotonic Capability Attenuation

    cs.CR 2026-05 unverdicted novelty 5.0

    ChainCaps uses monotonic capability attenuation via intersection of sink-specific budgets in a transparent proxy to reduce attack success on composed tool-using agents from 25-68% to 0-4.8% while keeping 96-100% benig...

  5. Authorization Propagation in Multi-Agent AI Systems: Identity Governance as Infrastructure

    cs.AI 2026-05 unverdicted novelty 5.0

    Multi-agent AI creates an authorization propagation problem not solved by prompt injection defenses or classical access control, requiring identity governance as continuously enforced infrastructure.

  6. The Importance of Out-of-Band Metadata for Safe Autonomous Agents: The Redpanda Agentic Data Plane

    cs.AI 2026-05 unverdicted novelty 3.0

    The Redpanda Agentic Data Plane uses out-of-band metadata channels to enforce data scoping, action constraints, and tamper-proof auditing on autonomous AI agents.

Reference graph

Works this paper leans on

54 extracted references · 3 canonical work pages · cited by 3 Pith papers

  1. [1]

    A neural proba- bilistic language model,

    Y . Bengio, R. Ducharme, P. Vincent, and C. Jauvin, “A neural proba- bilistic language model,”Journal of Machine Learning Research, vol. 3, no. Feb, pp. 1137–1155, 2003

    2003

  2. [2]

    Sequence to sequence learning with neural networks,

    I. Sutskever, O. Vinyals, and Q. V . Le, “Sequence to sequence learning with neural networks,” inAdvances in Neural Information Processing Systems, vol. 27, 2014, pp. 3104–3112. [Online]. Available: https://arxiv.org/abs/1409.3215

    Pith/arXiv arXiv 2014

  3. [3]

    Attention is all you need,

    A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser, and I. Polosukhin, “Attention is all you need,” in Advances in Neural Information Processing Systems, vol. 30, 2017. [Online]. Available: https://arxiv.org/abs/1706.03762

    Pith/arXiv arXiv 2017

  4. [4]

    React: Synergizing reasoning and acting in language models,

    S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y . Cao, “React: Synergizing reasoning and acting in language models,” in International Conference on Learning Representations (ICLR), 2023. [Online]. Available: https://par.nsf.gov/servlets/purl/10451467

    arXiv 2023

  5. [5]

    Toolformer: Language models can teach themselves to use tools,

    T. Schick, J. Dwivedi-Yu, R. Dessì, R. Raileanu, M. Lomeli, L. Zettlemoyer, N. Cancedda, and T. Scialom, “Toolformer: Language models can teach themselves to use tools,” inAdvances in Neural Information Processing Systems, vol. 36, 2023. [Online]. Available: https://arxiv.org/abs/2302.04761

    Pith/arXiv arXiv 2023

  6. [6]

    Prompt injection attacks against GPT-3,

    S. Willison, “Prompt injection attacks against GPT-3,” Sep. 2022. [On- line]. Available: https://simonwillison.net/2022/Sep/12/prompt-injection/

    2022

  7. [7]

    Why AI systems might never be secure,

    A. Hern, “Why AI systems might never be secure,”The Economist, Sep. 2025, “The gullibility of LLMs had been spotted before ChatGPT was even made public. In the summer of 2022, Willison and others independently coined the term ‘prompt injection’ to describe the behaviour.”. [Online]. Available: https://www.economist.com/science-and-technology/2025/ 09/23/w...

    2025

  8. [8]

    The dual LLM pattern for building AI assistants that can resist prompt injection,

    S. Willison, “The dual LLM pattern for building AI assistants that can resist prompt injection,” Apr. 2023. [Online]. Available: https://simonwillison.net/2023/Apr/25/dual-llm-pattern/

    2023

  9. [9]

    Defeating prompt injections by design,

    E. Debenedetti, I. Shumailov, T. Fan, J. Hayes, N. Carlini, D. Fabian, C. Kern, C. Shi, A. Terzis, and F. Tramèr, “Defeating prompt injections by design,” inIEEE Conference on Secure and Trustworthy Machine Learning (SaTML), 2026. [Online]. Available: https://arxiv.org/abs/2503.18813

    Pith/arXiv arXiv 2026

  10. [10]

    Agentdojo: A dynamic environment to evaluate prompt injection attacks and defenses for llm agents,

    E. Debenedetti, J. Zhang, M. Balunovic, L. Beurer-Kellner, M. Fischer, and F. Tramèr, “Agentdojo: A dynamic environment to evaluate prompt injection attacks and defenses for llm agents,”Advances in Neural Information Processing Systems, vol. 37, pp. 82 895–82 920, 2024

    2024

  11. [11]

    CaMeL offers a promising new direction for mitigating prompt injection attacks,

    S. Willison, “CaMeL offers a promising new direction for mitigating prompt injection attacks,” Apr. 2025. [Online]. Available: https: //simonwillison.net/2025/Apr/11/camel/

    2025

  12. [12]

    Call-by-name, call-by-value and theλ-calculus,

    G. D. Plotkin, “Call-by-name, call-by-value and theλ-calculus,” Theoretical Computer Science, vol. 1, no. 2, pp. 125–159, 1975. [Online]. Available: https://www.sciencedirect.com/science/article/pii/ 0304397575900171

    1975

  13. [13]

    A lattice model of secure information flow,

    D. E. Denning, “A lattice model of secure information flow,” Communications of the ACM, vol. 19, no. 5, pp. 236–243, 1976. [Online]. Available: https://dl.acm.org/doi/10.1145/360051.360056

    arXiv 1976

  14. [14]

    A functional view of imperative information flow,

    T. H. Austin, C. Flanagan, and M. Abadi, “A functional view of imperative information flow,” inProgramming Languages and Systems. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 34–49. [Online]. Available: https://link.springer.com/chapter/10.1007/ 978-3-642-35182-2_4

    2012

  15. [15]

    Securing AI agents with information-flow control,

    M. Costa, B. Köpf, A. Kolluri, A. Paverd, M. Russinovich, A. Salem, S. Tople, L. Wutschitz, and S. Zanella-Béguelin, “Securing AI agents with information-flow control,”arXiv preprint arXiv:2505.23643, 2025. [Online]. Available: https://arxiv.org/abs/2505.23643

    Pith/arXiv arXiv 2025

  16. [16]

    System-level defense against indirect prompt injection attacks: An information flow control perspective,

    F. Wu, E. Cecchetti, and C. Xiao, “System-level defense against indirect prompt injection attacks: An information flow control perspective,”

  17. [17]

    Security policies and security models,

    J. A. Goguen and J. Meseguer, “Security policies and security models,” inIEEE Symposium on Security and Privacy. IEEE, 1982, pp. 11–20. [Online]. Available: https://www.cs.purdue.edu/homes/ninghui/readings/ AccessControl/goguen_meseguer_82.pdf

    1982

  18. [18]

    Explicit secrecy: A policy for taint tracking,

    D. Schoepe, M. Balliu, B. C. Pierce, and A. Sabelfeld, “Explicit secrecy: A policy for taint tracking,” inIEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 2016, pp. 15–30

    2016

  19. [19]

    Opportunistically parallel lambda calculus,

    S. Mell, K. Kallas, S. Zdancewic, and O. Bastani, “Opportunistically parallel lambda calculus,”Proc. ACM Program. Lang., vol. 9, no. OOPSLA2, Oct. 2025. [Online]. Available: https://doi.org/10.1145/ 3763143

    2025

  20. [20]

    A fast, reliable, and secure programming language for llm agents with code actions,

    S. Mell, B. Zhang, D. Mell, S. Li, R. Ramalingam, N. Yu, S. Zdancewic, and O. Bastani, “A fast, reliable, and secure programming language for llm agents with code actions,” 2025. [Online]. Available: https://arxiv.org/abs/2506.12202

    Pith/arXiv arXiv 2025

  21. [21]

    A lambda-calculus foundation for universal probabilistic programming,

    J. Borgström, U. Dal Lago, A. D. Gordon, and M. Szymczak, “A lambda-calculus foundation for universal probabilistic programming,” inProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, 2016, pp. 33–46. [Online]. Available: https://dl.acm.org/doi/10.1145/2951913.2951942

    arXiv 2016

  22. [22]

    Efficient purely-dynamic information flow analysis (abstract only),

    T. H. Austin and C. Flanagan, “Efficient purely-dynamic information flow analysis (abstract only),”SIGPLAN Not., vol. 44, no. 8, p. 6, Dec

  23. [23]

    Certification of Programs for Secure Information Flow,

    D. E. Denning and P. J. Denning, “Certification of Programs for Secure Information Flow,”Comm. of the ACM, vol. 20, no. 7, pp. 504–513, Jul. 1977

    1977

  24. [24]

    Programming languages for information security,

    S. Zdancewic, “Programming languages for information security,” Ph.D. dissertation, Cornell University, August 2002. [Online]. Available: https://www.cis.upenn.edu/~stevez/papers/Zda02.pdf

    2002

  25. [25]

    Permissive dynamic information flow analysis,

    T. H. Austin and C. Flanagan, “Permissive dynamic information flow analysis,” inProceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, 2010, pp. 1–12. [Online]. Available: https://users.soe.ucsc.edu/~cormac/papers/ plas10.pdf

    2010

  26. [26]

    Generalizing permissive-upgrade in dynamic information flow analysis,

    A. Bichhawat, V . Rajani, D. Garg, and C. Hammer, “Generalizing permissive-upgrade in dynamic information flow analysis,” in Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security, ser. PLAS’14. New York, NY , USA: Association for Computing Machinery, 2014, p. 15–24. [Online]. Available: https://doi.org/10.1145/2637113.2637116

    arXiv 2014

  27. [27]

    On Dynamic Flow- Sensitive Floating-Label Systems ,

    P. Buiras, D. Stefan, and A. Russo, “ On Dynamic Flow- Sensitive Floating-Label Systems ,” in2014 IEEE 27th Computer Security Foundations Symposium (CSF). Los Alamitos, CA, USA: IEEE Computer Society, Jul. 2014, pp. 65–79. [Online]. Available: https://doi.ieeecomputersociety.org/10.1109/CSF.2014.13

    work page doi:10.1109/csf.2014.13 2014

  28. [28]

    Termination insensitive noninterference leaks more than just a bit,

    A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands, “Termination insensitive noninterference leaks more than just a bit,” inProc. European Symp. on Research in Computer Security, 2008. [Online]. Available: https://doi.org/10.1007/978-3-540-88313-5_22

    work page doi:10.1007/978-3-540-88313-5_22 2008

  29. [29]

    Lark: A parsing toolkit for Python,

    E. Shinan, “Lark: A parsing toolkit for Python,” 2017. [Online]. Available: https://github.com/lark-parser/lark

    2017

  30. [30]

    Responses API reference,

    OpenAI, “Responses API reference,” OpenAI Platform Documentation, 2025, accessed: 2026-01-24. [Online]. Available: https://platform. openai.com/docs/api-reference/responses

    2025

  31. [31]

    Church,The Calculi of Lambda Conversion, ser

    A. Church,The Calculi of Lambda Conversion, ser. Annals of Mathematics Studies. Princeton, NJ: Princeton University Press, 1941, no. 6. [Online]. Available: https://www.jstor.org/stable/j.ctt1b9x12d

    1941

  32. [32]

    History of lambda-calculus and combinatory logic,

    F. Cardone and J. R. Hindley, “History of lambda-calculus and combinatory logic,” inLogic from Russell to Church (Handbook of the History of Logic, Volume 5), D. M. Gabbay and J. Woods, Eds. Amsterdam: Elsevier, 2006, pp. 723–817. [Online]. Available: http://www.users.waitrose.com/~hindley/SomePapers_PDFs/ 2006CarHin,HistlamRp.pdf

    2006

  33. [33]

    Introduction to the CUCH,

    C. Böhm and W. Gross, “Introduction to the CUCH,” inAutomata Theory, E. R. Caianiello, Ed. New York: Academic Press, 1966, pp. 35–65

    1966

  34. [34]

    A correspondence between ALGOL 60 and Church’s lambda-notation,

    P. J. Landin, “A correspondence between ALGOL 60 and Church’s lambda-notation,”Communications of the ACM, vol. 8, no. 2–3, pp. 89–101, 158–165, feb–mar 1965. [Online]. Available: https: //dl.acm.org/doi/10.1145/363744.363749 13

    arXiv 1965

  35. [35]

    Fundamental concepts in programming languages,

    C. Strachey, “Fundamental concepts in programming languages,” Higher-Order and Symbolic Computation, vol. 13, pp. 11–49, 2000, lecture notes from 1967, first formally published in 2000. [Online]. Available: https://link.springer.com/article/10.1023/A:1010000313106

    work page doi:10.1023/a:1010000313106 2000

  36. [36]

    Analysis and caching of dependencies,

    M. Abadi, B. W. Lampson, and J.-J. Lévy, “Analysis and caching of dependencies,” inProceedings of the First ACM SIGPLAN International Conference on Functional Programming, ser. ICFP ’96. New York, NY , USA: Association for Computing Machinery, 1996, pp. 83–91. [Online]. Available: https://doi.org/10.1145/232627.232638

    arXiv 1996

  37. [37]

    From fine- to coarse-grained dynamic information flow control and back,

    M. Vassena, A. Russo, D. Garg, V . Rajani, and D. Stefan, “From fine- to coarse-grained dynamic information flow control and back,”Proc. ACM Program. Lang., vol. 3, no. POPL, Jan. 2019. [Online]. Available: https://doi.org/10.1145/3290389

    doi:10.1145/3290389 2019

  38. [38]

    Flexible dynamic information flow control in haskell,

    D. Stefan, A. Russo, J. C. Mitchell, and D. Mazières, “Flexible dynamic information flow control in haskell,” inProceedings of the 4th ACM Symposium on Haskell, ser. Haskell ’11. New York, NY , USA: Association for Computing Machinery, 2011, p. 95–106. [Online]. Available: https://doi.org/10.1145/2034675.2034688

    arXiv 2011

  39. [39]

    Beyond labels: Permissiveness for dynamic information flow enforcement,

    E. Kozyri, F. B. Schneider, A. Bedford, J. Desharnais, and N. Tawbi, “Beyond labels: Permissiveness for dynamic information flow enforcement,” in2019 IEEE 32nd Computer Security Foundations Symposium (CSF), 2019, pp. 351–35 115. [Online]. Available: https: //ieeexplore.ieee.org/document/8823779

    arXiv 2019

  40. [40]

    Prompt flow integrity to prevent privilege escalation in llm agents,

    J. Kim, W. Choi, and B. Lee, “Prompt flow integrity to prevent privilege escalation in llm agents,” 2025. [Online]. Available: https://arxiv.org/abs/2503.15547

    Pith/arXiv arXiv 2025

  41. [41]

    Ace: A security architecture for llm-integrated app systems,

    E. Li, T. Mallick, E. Rose, W. Robertson, A. Oprea, and C. Nita-Rotaru, “Ace: A security architecture for llm-integrated app systems,” 2025. [Online]. Available: https://arxiv.org/abs/2504.20984

    Pith/arXiv arXiv 2025

  42. [42]

    Not what you’ve signed up for: Compromising real-world LLM- integrated applications with indirect prompt injection,

    K. Greshake, S. Abdelnabi, S. Mishra, C. Endres, T. Holz, and M. Fritz, “Not what you’ve signed up for: Compromising real-world LLM- integrated applications with indirect prompt injection,” inProceedings of the 16th ACM Workshop on Artificial Intelligence and Security (AISec), 2023, pp. 79–90. [Online]. Available: https://arxiv.org/abs/2302.12173

    Pith/arXiv arXiv 2023

  43. [43]

    Formalizing and benchmarking prompt injection attacks and defenses,

    Y . Liu, Y . Jia, R. Geng, J. Jia, and N. Z. Gong, “Formalizing and benchmarking prompt injection attacks and defenses,” in33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 2607–2624. [Online]. Available: https://arxiv.org/abs/2310.12815

    arXiv 2024

  44. [44]

    Defending against indirect prompt injection attacks with spotlighting,

    K. Hines, G. Lopez, M. Hall, F. Zarfati, Y . Zunger, and E. Kiciman, “Defending against indirect prompt injection attacks with spotlighting,” inProceedings of the Conference on Applied Machine Learning in Information Security (CAMLIS), 2024, pp. 48–62. [Online]. Available: https://arxiv.org/abs/2403.14720

    Pith/arXiv arXiv 2024

  45. [45]

    The task shield: Enforcing task alignment to defend against indirect prompt injection in LLM agents,

    F. Jia, T. Wu, X. Qin, and A. Squicciarini, “The task shield: Enforcing task alignment to defend against indirect prompt injection in LLM agents,” inProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (ACL), 2025. [Online]. Available: https://arxiv.org/abs/2412.16682

    Pith/arXiv arXiv 2025

  46. [47]

    SWE-Agent: Agent-computer interfaces enable automated software engineering,

    J. Yang, C. E. Jimenez, A. Wettig, K. Lieret, S. Yao, K. Narasimhan, and O. Press, “SWE-Agent: Agent-computer interfaces enable automated software engineering,”Advances in Neural Information Processing Sys- tems, vol. 37, pp. 50 528–50 652, 2024

    2024

  47. [48]

    Types for dyadic interaction,

    K. Honda, “Types for dyadic interaction,” inCONCUR’93, ser. Lecture Notes in Computer Science, vol. 715. Springer, 1993, pp. 509–523. [Online]. Available: https://doi.org/10.1007/3-540-57208-2_35

    doi:10.1007/3-540-57208-2_35 1993

  48. [49]

    Language primitives and type discipline for structured communication-based programming,

    K. Honda, V . T. Vasconcelos, and M. Kubo, “Language primitives and type discipline for structured communication-based programming,” in Programming Languages and Systems (ESOP’98), ser. Lecture Notes in Computer Science, vol. 1381. Springer, 1998, pp. 122–138. [Online]. Available: https://doi.org/10.1007/BFb0053567

    doi:10.1007/bfb0053567 1998

  49. [50]

    The hottest new programming language is English,

    A. Karpathy, “The hottest new programming language is English,” Jan. 2023, post on X (formerly Twitter). [Online]. Available: https://x.com/karpathy/status/1617979122625712128

    arXiv 2023

  50. [51]

    A sound type system for secure flow analysis,

    D. V olpano, C. Irvine, and G. Smith, “A sound type system for secure flow analysis,” inJournal of Computer Security, vol. 4, no. 2-3. IOS Press, 1996, pp. 167–187. [Online]. Available: https://users.cs.fiu.edu/~smithg/papers/jcs96.pdf 14 APPENDIX Contents: A. Proof of the Main Theorem (Theorem 1) B. Encoding of derived expressions C. Prelude D. Code list...

    1996

  51. [55]

    {e}

    Moreover, Lemma 4(1) givespc⊑ label(Vi); sincepc̸⊑k, we havelabel(V i)̸⊑kfori∈ {0,1}. By the definition of∼ k on values,V 0 ∼k V1. Restatement of Theorem 1The following sublanguages satisfy TINI: (1)expressions built without?; (2)expressions which use only one non-bottom label, and (3)expressions in which?occurs only in the form ofassert statements or str...

  52. [2009]

    Available: https://doi.org/10.1145/1667209.1667220

    [Online]. Available: https://doi.org/10.1145/1667209.1667220

    arXiv

  53. [2021]

    Available: https://arxiv.org/abs/2107.03374

    [Online]. Available: https://arxiv.org/abs/2107.03374

    Pith/arXiv arXiv

  54. [2024]

    Available: https://arxiv.org/abs/2409.19091

    [Online]. Available: https://arxiv.org/abs/2409.19091

    Pith/arXiv arXiv