Paper deep dive
Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation
Paul Kronlund-Drouault
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Constrained decoding can enforce regular or context-free output formats, but many program-generation failures are semantic: scope, typing, and declaration effects depend on context. We present semantic grammar specifications, a declarative formalism that attaches such constraints to a context-free surface and executes them during Earley descent. Our implementation enforces \emph{safe pruning}: it rejects only prefixes whose semantic contradictions cannot be repaired by any continuation. A separate, grammar-dependent, \emph{dead-end freedom} property guarantees the existence of a realizable witness for each remaining branch. We give simple sufficient conditions based on surface productivity, type coverage, and left-to-right constraint flow. Our finite-lambda, core ML, and C-like fragments satisfy them, while the STLC instance used in our experiments does not: plain STLC can violate type coverage, and we show how restricting its type universe recovers it. A tokenizer-lifting lemma carries character-level witnesses to token sequences under an explicit vocabulary-coverage hypothesis. We validate the implementation differentially against production compilers (\texttt{ocamlc}, \texttt{cc}). Across every prefix of 65 compiler-valid programs we observe zero false prunes. The semantic oracle localizes 25/30 invalid programs mid-stream, against 0/30 for a syntax-only oracle, and agrees on 42/42 recursion probes. A twelve-model generation study, including a matched semantic-versus-syntactic ablation for nine models, finds nonnegative observed semantic-minus-syntactic point estimates for every model-language pair, with maxima of $+15.2$ points on STLC task correctness and $+14.3$ points on ML validity.
Tags
Links
- Source: https://arxiv.org/abs/2609.35425v1
- Canonical: https://arxiv.org/abs/2609.35425v1
Trouble viewing inline? Open PDF directly →
Full Text
61,608 characters extracted from source content.
Expand or collapse full text
Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation DOI: 10.1145/3843750.3843841ISBN: 979-8-4007-2986-7/2026/10Conference: Proceedings of the 2nd ACM SIGPLAN International Workshop on Language Models and Programming Languages; October 4–9, 2026; Oakland, CA, USAProceedings of the 2nd ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL ’26), October 4–9, 2026, Oakland, CA, USAsplashws26lmplmain-p30-pCCS: Theory of computation Grammars and context-free languagesCCS: Software and its engineering Formal language definitionsCCS: Software and its engineering Software testing and debuggingCCS: Computing methodologies Natural language processing Paul Kronlund-Drouault Affiliation: ENS de Lyon, Lyon, France Affiliation: Unsuspicious Industries, Paris, France Affiliation: Université de Lille, Lille, France email: pkd@unsuspicious.org Received 2026-08-14 Abstract. Constrained decoding can enforce regular or context-free output formats, but many program-generation failures are semantic: scope, typing, and declaration effects depend on context. We present semantic grammar specifications, a declarative formalism that attaches such constraints to a context-free surface and executes them during Earley descent. Our implementation enforces safe pruning: it rejects only prefixes whose semantic contradictions cannot be repaired by any continuation. A separate, grammar-dependent, dead-end freedom property guarantees the existence of a realizable witness for each remaining branch. We give simple sufficient conditions based on surface productivity, type coverage, and left-to-right constraint flow. Our finite-lambda, core ML, and C-like fragments satisfy them, while the STLC instance used in our experiments does not: plain STLC can violate type coverage, and we show how restricting its type universe recovers it. A tokenizer-lifting lemma carries character-level witnesses to token sequences under an explicit vocabulary-coverage hypothesis. We validate the implementation differentially against production compilers (ocamlc, c). Across every prefix of 65 compiler-valid programs we observe zero false prunes. The semantic oracle localizes 25/30 invalid programs mid-stream, against 0/30 for a syntax-only oracle, and agrees on 42/42 recursion probes. A twelve-model generation study, including a matched semantic-versus-syntactic ablation for nine models, finds nonnegative observed semantic-minus-syntactic point estimates for every model-language pair, with maxima of +15.2+15.2 points on STLC task correctness and +14.3+14.3 points on ML validity. Keywords: constrained decoding, semantic prefix grammars, attribute grammars, differential testing, large language models †c-license: by 1. Introduction Grammar-constrained decoding has by now entered inference infrastructure, with libraries such as Outlines (Willard and Louf, 2023), DOMINO (Beurer-Kellner et al., 2024), and Formatron (Sun et al., 2025) which mask a model’s vocabulary so that every emitted prefix extends to output in a regular or context-free language, giving a structural guarantee of completability. The constraints they express are nonetheless weak relative to how models actually fail. Syntax-only constraints do not address consequential program-generation failures such as scope, type compatibility, and declaration effects, none of which a grammar mask can express. Lifting the guarantee to semantic constraints gives two distinct properties: (1) safe pruning: no prefix with a semantically valid completion is rejected (2) dead-end freedom: every retained prefix still has such a completion The first protects the model’s valid continuations while the second protects the decoding loop from being walked into a state where no token is admissible. They are different theorems with different hypotheses. We structure this paper around the following question: When may a semantic prefix oracle reject an LLM continuation without hiding a valid program, and how do we validate that the implementation actually respects that contract? As a working example, take the finite lambda instance of §3.2. Under its constraints, a model that has decoded let x : Int = may still emit a digit, an open parenthesis, or any Int in scope, but the token true is masked out: the annotation has fixed the demanded type and the boolean literal’s type is fixed too. This is where semantics is needed, since let x : Int = true; is a perfectly good parse in the underlying context-free grammar. Our declarative format attaches typing rules to a context-free surface. The rules compile to a language-parametric IR over first-order terms, pattern ascription, syntactic unification, and finite right-bound context effects. Aufbau executes this IR during Earley descent and rejects a path only after a stable semantic contradiction. The kernel has no built-in notion of type, function, or arrow. Those meanings come from each grammar’s constructors and shared holes. Safe pruning is therefore a property of the oracle. Dead-end freedom is a stronger property of particular grammars. In §2.3 we give three sufficient conditions, show that the ML and C-like instances satisfy them, and show why the STLC instance used in our experiments does not. Because a proof of the rejection rule does not rule out implementation bugs, we also validate Aufbau differentially against production compilers sharing none of our code. P7 then measures what the semantic layer buys over the same mask with typing removed. This paper contributes: • A semantic-prefix formalism that separates safe pruning from dead-end freedom, with a safe-pruning theorem, simple sufficient conditions for dead-end freedom, and a tokenizer-lifting lemma under an explicit vocabulary-coverage hypothesis (§2, §3) • A language-parametric implementation (Aufbau/P7, with STLC, finite-lambda, core ML, C-like, and typed tool-DSL instances in three surface dialects) and prefix-by-prefix differential validation against ocamlc and c: zero false prunes over every prefix of 65 in-fragment valid programs, 42/42 on a recursion probe, mid-stream error localization at 25/30 vs. 0/30 for a syntax-only oracle (§3–§4.1) • A twelve-model generation study containing a matched semantic-versus-syntactic ablation for the nine models that ran both arms, 3,693 graded attempts in total, holding parser, sampler, tokenizer bridge, and surface grammar fixed, with per-language validity and correctness metrics reported separately, together with exploratory observations on reasoning-then-constrained scheduling, rejection–uncertainty association, and multi-turn tool episodes (§4.2). The artifact contains the implementation, specifications, data, and commands used for the reported measurements. 2. The Constraint Model 2.1. Grammar Specifications We fix an alphabet Σ and write L⊆Σ∗L for a language. A prefix s is completable for L when ss′∈Lss ∈ L for some s′s . Prefix parsing accepts exactly the completable prefixes of the surface syntax. The surface parser keeps branches compatible with the consumed input, and the semantic layer removes branches carrying a stable contradiction. Writing RGR_G for the prefixes retained by Aufbau, the guarantee proved below (§2.3) is the one-sided inclusion Pref(LG)⊆RG,Pref(LG)=s∣∃r.sr∈LG.Pref(L_G) R_G, (L_G)=\s ∃ r.\;sr∈ L_G\. Definition 2.1 (Semantic grammar specification). A semantic grammar specification (what an .auf file can represent) is a tuple G=(N,T,P,S,Θ,,ℬ)G=(N,T,P,S, ,T,B): nonterminals N, terminal recognizers T, productions P, start symbol S, semantic rules Θ , a partial map :N⇀ΘT:N attaching a rule to a nonterminal, and binding identifiers ℬB. A production for n is a sequence α1[b1]⋯αm[bm] _1[b_1]·s _m[b_m] where each αi∈T∪N _i∈ T∪ N and each bi∈ℬ∪εb_i ∪\ \ names the child’s evidence for use by a rule. We reserve semantic prefix grammar for the subclass additionally satisfying the three conditions of §2.3 that guarantee witness construction. Bindings are annotations only, and do not affect the context-free structure. Terminals are matched through a segment interface returning a status in ,\ Prefix, , Exact, Extensible\ together with a regular residual, the derivative of the recognizer after the consumed segment (Brzozowski, 1964; Owens et al., 2009). The minimal example, used throughout: Id →ℛ([A-Za-z][A-Za-z0-9]∗) ( [A-Za-z][A-Za-z0-9] ) Type →Id∣Type‘→’Type∣‘(’Type‘)’ \;`$→$'\;Type `('\,Type\,`)' Var →Id[x] [x] (var) ( var) Lam →‘λ’Id[a]‘:’Type[t]‘.’Expr[e] →`$λ$'\,Id[a]\,`:'\,Type[t]\,`.'\,Expr[e] (lam) ( lam) App →Expr[l]Expr[r] [l]\;Expr[r] (app) ( app) Expr →Var∣Lam∣App with one rule per annotated nonterminal, each a set of ascriptions over shared holes , A, B: x:inΓ:(var)Γ[a:t]⊢e::t→(lam)l:→r::(app) x: A\ in\ \,:\, A\,( var)\;\; [a:t] e: B\,:\,t→ B\,( lam)\;\; l: A→ B 9.24994ptr: A\,:\, B\,( app) The app rule has no idea what a function is. Its premise l:→l: A→ B is one constructor pattern: → is a constructor because the grammar’s type fragment wrote it, and , A, B bind its subterms. There is no separate algebra of types, leaves are regular languages, and the arrow means only what hole-sharing across the three rules makes it mean. The inference notation is a front end to a small IR of term evaluation, ascription, equality, context membership, scoped extension, and right-bound effects, and the same IR runs the ML, C, and tool instances with no distinguished type or function instruction. 2.2. Evidence and Constraint Graphs To keep the mechanism language-parametric, semantic evidence is represented only by terms over the grammar’s signature, with ascription for checking a term against an expected pattern and first-order unification as the sole rewriting mechanism (Robinson, 1965; Martelli and Montanari, 1982). Context lookup, type equality, and structural matching are all ascriptions discharged by unification. Equality τ1=τ2 _1= _2 is τ1:τ2 _1: _2. Membership x∈Γx∈ is x:x: A solved against Γ . A shape such as → A→ B is matched constructor-against-constructor with each hole bound by position, with no decomposition step and no built-in notion of domain or codomain. Parsing a prefix yields an AST whose nodes carry, at bound positions, evidence: a status in ,,\ Exact, Prefix, Extensible\ propagated bottom-up, a type term possibly containing holes, an exported context effect, and a binding map sending each binding either to (ν) Resolved(ν) (the child’s evidence, once the dot has passed it) or Pending (the child is past the right frontier). A binding moves from Pending to Resolved, never the reverse. This is the available/unavailable split of incremental attribute grammars (Demers et al., 1981) and the typed-hole reading of an unfilled position (Omar et al., 2017). Rules relate evidence directly, so semantic information forms a graph over evidence rather than a tree. Firing a rule emits one unification edge per premise plus a conclusion edge, and holes shared between ascriptions become equality edges. This is the constraint-generation reading of type inference where a typing system is a set of unification constraints over a partial program. A vertex is frontier when it still carries an incomplete-input signal (status Prefix/ Extensible, or a Pending binding). The graph at prefix s, written (s)G(s), is open when some edge touches a frontier vertex and closed when it is not open and the solver finds no contradiction. The parser builds and solves this graph during Earley descent rather than after parsing. A stable contradiction removes that item immediately, while unresolved frontier evidence remains in the chart. Context effects are right-bound. Only an Exact node exports a declaration into the context its right siblings see. Proposition 2.2 (Fixed-prefix decidability). Let G be finite with regular terminals, and let every semantic rule compile to a finite straight-line IR program interpreted in the free first-order theory with the occurs check and no declared rewrites. Compute the nullable nonterminals by least fixed point and define the zero-consumption left-corner relation A→0BA _0B: some production of A can reach an occurrence of B after a prefix of nullable symbols. Suppose the →0 _0 graph restricted to nonterminals reachable from S is acyclic, and, separately, that every reachable nonterminal is productive (derives some finite terminal string). Then evaluation of any finite prefix and masking over any finite candidate set are decidable. Proof (sketch). Earley parsing over a finite input has a finite chart of item cores. Semantic elaboration can multiply items only by re-deriving the same core with different evidence. Acyclicity of →0 _0 bounds the number of rule firings attributable to any span, so each core carries finitely many semantic refinements and context effects. Terms are finite, regular-leaf intersection is decidable, and first-order unification terminates with the occurs check. Semantic pruning only removes annotated items, so the annotated chart reaches a fixed point, and the same procedure applied to each member of a finite candidate set terminates. ∎ Zero-consumption is needed, because a unit cycle such as A→BA→ B, B→A|xB→ A x consumes no input while its rules wrap evidence on every traversal, giving one finite span unboundedly many annotations. Productivity covers a separate failure mode, since a consuming cycle can still be unproductive, as S→xS→ x\,S is. Both are decidable by least-fixed-point computation and are checked when a grammar is loaded. The proposition decides whether a fixed finite continuation survives the semantic Earley chart. Whether an arbitrary prefix has some valid suffix is a different question, and needs the analysis below. Declared normalization rewrites are outside Proposition 2.2, since they need separate termination and confluence arguments. 2.3. Verdicts: Safe Pruning and Dead-End Freedom Definition 2.3 (Witness, denotation, verdict). A witness for a prefix s is r∈Σ∗r∈ such that srsr admits a complete parse of the start symbol whose graph (sr)G(sr) is closed and consistent. The denotation (s)D(s) is the set of witnesses. The semantically valid language LGL_G is the set of complete inputs with an empty-witness parse. The evaluator returns ((s))=Satisfiedclosed and consistent,Loststable contradiction,Liveotherwise.eval(G(s))= cases Satisfied&closed and consistent,\\ Lost&stable contradiction,\\ Live&otherwise. cases A contradiction is stable when later input cannot repair it. This includes rigid constructor clashes, regular-leaf clashes, occurs-check failures, and failed lookups in the fixed left context. Ambiguity is existential: a prefix is Lost only when every compatible branch is Lost. Theorem 2.4 (Safe pruning). Aufbau never rejects a prefix that has a witness. Proof. Every rejection is justified by a stable contradiction on every compatible branch. Extending a branch can instantiate unresolved holes, refine regular residuals as more input is consumed, and append right-bound context effects. The rejection forms above are monotone under those operations: a rigid constructor clash remains a clash, an empty regular intersection cannot be restored by further refinement, an occurs-check failure cannot be repaired by later substitution, and a failed lookup in the fixed left context cannot be repaired by declarations exported to the right. Thus a contradiction classified as stable persists on every extension of that branch. If s had a witness r, the complete consistent parse of srsr would restrict to a compatible branch at s that is not Lost, contradicting rejection. ∎ The implementation is conservative about information that is not yet fixed. In particular, prediction-time checks use only constraints already determined by the consumed prefix. Missing information can therefore delay a rejection, but it cannot create one. This matters for dead-end freedom, not for safe pruning. Dead-end freedom is a property of a grammar in addition to the oracle. A Live prefix has not contradicted the grammar, but it may still have no completion. Plain STLC gives the simplest example. With distinct atomic types A and B, the prefix λf:A→B.f(CLOSEλ f:A→B.\ f( demands a term of type A. If the language has no closed term of type A, the prefix is Live but has no witness. For the typed grammars in this paper, the relevant notion of inhabitation is simply type coverage: every type that can be demanded at a reachable prefix has some finite closed term of that type. A universal inhabitant is one way to obtain coverage, but it is not required. Throughout, a parser branch, nonterminal, regular residual, or type demand is reachable when it occurs after consuming some finite input prefix from the start symbol on a compatible branch, before that branch becomes Lost. Definition 2.5 (Dead-end-free grammar class). We use the following sufficient conditions for dead-end freedom. (P) Surface productivity. Every reachable nonterminal has a finite completion, and every reachable regular residual is nonempty. (T) Type coverage. Every reachable type demand has a finite closed realizer whose construction does not invalidate the already fixed left context. (F) Left-to-right constraint flow. A child’s semantic obligations are determined by the parent demand, the fixed context, and children to its left. Later children do not constrain earlier ones. Theorem 2.6 (Dead-end freedom under coverage). A grammar satisfying (P), (T), and (F) is dead-end free: every Live prefix has a witness. Proof sketch. Complete the leftmost unfinished position repeatedly. Condition (P) closes purely syntactic and regular positions. When a typed expression is required, (F) makes its demanded type depend only on information already fixed to its left, and (T) supplies a finite closed term of that type. Repeating this process moves strictly rightward and eventually closes the parse. The chosen terms satisfy the demands under which they were inserted, so the resulting completion is consistent. ∎ The conditions are deliberately sufficient rather than a characterization of every grammar on which Aufbau happens to avoid dead ends. They are useful because they separate the oracle property from the language property. Safe pruning holds independently. Dead-end freedom follows once a grammar has productive syntax, type coverage, and left-to-right semantic flow. The examples make the boundary concrete, and the boundary runs through our own instances. Our STLC instance (§3.2) does not satisfy (T): its base-type universe is unrestricted, so an atomic type may have no closed inhabitant, and the λf:A→B.f(CLOSEλ f:A→B.\ f( prefix above is a prefix of that grammar. Coverage is recoverable by construction: restrict the base-type universe to a finite set in which every base type has a literal. The literals cover the base types, and arrow types follow inductively, since a closed realizer eBe_B of B makes (x:A)⇒eB(x:A) e_B a closed realizer of A→BA→ B. The finite-lambda instance below uses exactly this construction. We did not run the reported STLC experiments on that restricted instance. Core ML has a simpler cover because assert false can be assigned every expression type. The C-like fragment also covers every reachable expression-type demand in its fragment: scalar types have literals, and explicit casts from a scalar literal realize pointer types and the other concrete expression types admitted by the grammar. The tool DSL has no comparable universal cover. With an empty context, let s = summarize( demands a docs value, but the grammar has no closed docs literal, so the prefix can remain Live with no completion. Nothing in this argument requires the implementation to decide (P), (T), and (F) automatically. They state when the stronger dead-end-free guarantee applies. The implementation itself only relies on the safe-pruning contract. 2.4. Worked Example Figure 1 illustrates the three verdicts. The complete term resolves x in the fixed context and closes the graph. A pending body leaves the graph open and therefore Live, without guaranteeing a witness. The exact variable y fails lookup in Γ=[x:] =[x: int], yielding a stable contradiction that syntax alone cannot detect. λx:int.xλ x:int.\;x SatisfiedLam (lam) : int→ (var) : intbodyx↦intx intin Γ=[x:] =[x: int](a)λx:int.λ x:int. LiveLam (lam) : int→ Bbody eePendingbody(b)λx:int.yλ x:int.\;y LostLam (lam) : intVar (var)bodyy∉Γy∉ Γ=[x:] =[x: int](c) Figure 1. The oracle’s evidence on three prefixes of the minimal grammar. Gray right-angle links show AST structure, colored links semantic evidence. The complete term closes at → int→ int. The missing body stays Pending. The exact variable y fails lookup in Γ=[x:] =[x: int], making the last prefix Lost.Three evidence graphs. The complete term lambda x colon int dot x is Satisfied with type int to int, lambda x colon int with a pending body is Live and lambda x colon int dot y is Lost because y is absent from the context. 3. Aufbau, P7, and the Instances 3.1. Architecture A language definition is lowered into Aufbau’s semantic grammar IR, productions, regular terminals, binding positions, compiled rule programs, context effects, with .auf as one readable front end and the API able to construct the same IR directly. Aufbau executes it inside an Earley parser (Earley, 1970) whose items carry the evidence and constraint graph of §2.2. The entry point try_feed extends the current prefix by a candidate string and returns the three-valued verdict. P7 puts this oracle in the decoding loop (Figure 2). LLMmodel P7controller Aufbauoracle tokentry_feedverdictLostexclude and resample Livecommit and continue Satisfiedcommit and finish resample Figure 2. P7 constrained-decoding architecture. The model proposes a token, P7 submits it to the Aufbau prefix oracle, and the oracle returns one of three verdicts: Lost is excluded and resampled, Live is committed and decoding continues, Satisfied completes the derivation.An LLM sends a proposed token to P7, which calls the Aufbau oracle. Lost excludes and resamples the token, Live commits it and continues, and Satisfied commits it and finishes. Two properties of the loop matter below. The mask never forces completion: the model’s own stop tokens stay admissible mid-derivation, so §4.2 counts abandonments rather than hiding them. The mask prunes rather than repairs: given a model with no useful solution, it can turn free-form garbage into well-formed garbage that still fails grading. Tokenizer lifting. P7 feeds Aufbau tokens, not characters, so the guarantees above must cross that boundary. Write ΣG=⋃R∈Talph(R) _G= _R∈ Talph(R) for the union of the recognizers’ alphabets, ℓ:V→ΣG∗ :V→ _G for the exact spelling map on ordinary text tokens of the vocabulary V (control tokens and eos follow the completion policy above), and LV=ℓ(v)∣v∈VL_V=\ (v) v∈ V\. The coverage hypothesis ΣG⊆LV∗ _G L_V gives ΣG∗⊆LV∗ _G L_V , since LV∗L_V is closed under concatenation. Lemma 3.1 (Tokenizer lifting). Under exact spelling (the oracle consumes, byte-for-byte, the text the model conditions on) and coverage, every character-level witness factors into a finite token sequence, and regular derivatives carry the oracle’s state across a token ending inside a terminal recognizer. Character-level witness existence therefore lifts to token-sequence reachability. Proof. Coverage factors the witness into a concatenation of spellings ℓ(v1)⋯ℓ(vk) (v_1)·s (v_k), exactly the string P7 submits token by token, and composing the recognizer’s derivative across v1,…,vkv_1,…,v_k reaches the residual the character-level run would. ∎ 3.2. Language Instances STLC A monomorphic simply-typed lambda calculus with mandatory binder annotations, used both by the oracle’s validation harnesses and as the STLC arm of the generation study. Its base-type universe is unrestricted, so this instance does not satisfy the type-coverage condition (T) of §2.3 and we make no dead-end-freedom claim for it: the λf:A→B.f(CLOSEλ f:A→B.\ f( counterexample is a prefix of this grammar. Safe pruning applies to it exactly as to every other instance. Finite Lambda (fun.auf). A variant of the lambda calculus with modern surface syntax, let-bindings, and a base-type universe restricted to Int, Bool, and Float, each equipped with literals. These literals cover the base types. Function types are covered inductively: if eBe_B is a closed realizer of B, then (x: A) => eBe_B is a closed realizer of A→BA→ B. Together with productive syntax and left-to-right constraint flow, the instance therefore satisfies (P), (T), and (F), unlike the unrestricted STLC instance used in the experiments. Core ML (ml.auf). A monomorphic ML fragment with let/let rec, functions, application, integers, booleans, comparison and arithmetic, lists (T list, cons, []), if/then/else, and assert false. The concrete syntax is a strict OCaml subset, so every accepted program feeds ocamlc with no translation. This makes differential prefix validation possible (§4.1). The axiom assert false: assert false: A is a universal expression inhabitant, so every reachable ML expression-type demand is covered. Checking-mode let rec is incremental because its signature is fixed before the body streams. A C-like fragment (c.auf). A typed C-like fragment whose accepted output is graded by c -fsyntax-only: declarations and assignment, typed functions and calls, if, while, and for, arithmetic and comparison over int, float, and char, pointers with address-of and dereference, and explicit casts. The fragment threads each function’s declared return type through an ambient context entry and checks every return against it, admitting a bare return; only in a void function.11 1 The return-type check postdates the generation study of §4.2, which ran on the earlier version of c.auf without it. The reported C generation numbers are therefore for that earlier grammar and rerunning them is future work. §4.2 repeats this caveat where the numbers appear. We still call it C-like deliberately: it does not prove that every path through a non-void function returns, does not constrain the operand of a cast or of address-of, and its demanded-type universe includes void and unbounded pointer depth, so Aufbau-accepted programs are not guaranteed to be accepted, or accepted without diagnostics, by a C compiler. For dead-end freedom, the relevant point is narrower than full C validity. Every reachable expression-type demand in this fragment has a closed realization: scalar types have literals, while explicit casts from a scalar literal realize the pointer types admitted by the grammar. Together with the fragment’s productive statement forms and left-to-right declaration flow, this gives the coverage used in Theorem 2.6. The differential harness of §4.1 separately checks compatibility with c. Two design points carry the semantics. A two-sort type discipline keeps the concrete sort CType (scalars and pointers, what a cast or declaration can spell) distinct from the internal signature sort that types functions. The latter is unreachable from concrete syntax, so no source expression can demand a function-shaped type. And definition-before-use holds at translation-unit granularity: a call is checked against a signature already exported by an earlier definition’s right-bound effect, which a left-to-right oracle handles without lookahead because the definition precedes the call in the token stream. Declarative boundary: self-recursion. Inference-mode recursion cannot be declared in this fragment. let rec without an annotation was implemented and dropped after some empirical failure evidence. The problem is that the recursive call races the still-streaming parameter list to resolve the signature metavariable, and an early unification can commit it to a shape the header later contradicts, producing a false prune rather than a real error. Checking-mode recursion, whose signature is exact before the body opens, has no such race, so the declarable fragment admits checking-mode program recursion only and inference-mode program recursion is excluded as a restriction of the fragment. It could theoretically be implemented but would require dropping the level of constraints which isn’t very interesting here. This important limitation was found by our test system probing ocamlc against the oracle. Indeed, some experiments on recursion corners surfaced the discrepancy (§4.1). The instrumentation that rejects the model’s tokens is what caught the grammar author. This establishes the importance of our differential certification approach for implementation correctness. The agentic tool DSL dialects. The third instance exercises the semantic layer as an agent harness. Constrained decoding is usually evaluated on single-shot synthesis, but multi-turn tool use, where the typed context grows as the episode runs, is the natural application for a typed oracle. tool.auf is an invented typed pipeline language over a fixed registry (search: string→ , summarize: docs→ , count: docs→ , format: int→ ) with let-sequencing and return. Being invented, it has no pretraining prior and no external compiler, so an episode is graded by the value its return evaluates to against the registry’s real implementations rather than by well-typedness. Each turn is one constrained step. The binding it introduces is pushed into Γ , so turn n+1n+1 decodes under the types established by turns 1..n1..n, threading the constraint graph of §2.2 across the episode. Three dialects share one type discipline: a C-like let syntax (tool.auf), S-expressions (tool_sexpr.auf), and XML elements (tool_xml.auf). Only the surface varies, so the dialect axis separates semantic discipline from syntax priors and tokenizer alignment. The dialects also show why registry reachability is weaker than type coverage. With an empty context, let s = summarize( is Live with no completion because the demanded docs argument has no literal form and no binding supplies one. We therefore make no dead-end-freedom claim for the tool DSLs. A 51-case harness checks the checker given a witness by injecting a binding of the demanded type at each demanding argument position and confirming acceptance. 4. Empirical Findings The evidence comes in two tiers with different epistemic status, and we keep them apart. Tier 1 (§4.1) tests the oracle: CPU-only, deterministic, regenerable byte-for-byte by a reviewer with no GPU. Tier 2 (§4.2) measures what the oracle buys in generation: GPU runs over open models, single greedy attempts, graded by per-language metrics that are deliberately not pooled into one accuracy (§4.2 defines each). 4.1. Differential Prefix Validation The oracle’s verdicts are compared prefix by prefix against a production compiler that shares none of our code: ocamlc for the ML instance and c for the C instance. These are finite, hand-selected test cohorts, so the results validate rather than certify. The harness extends mechanically. Safe pruning (Theorem 2.4) applies to every instance. The cohorts below add finite external evidence for the ML and C implementations, the two instances with production-compiler comparators. Differential testing can expose implementation bugs, but finite cohorts are not an exhaustive correctness proof. Theorem 2.4 is in any case a paper proof of the rejection discipline, and the shipped engine is an optimized realization of it: these cohorts check selected end-to-end compatibility properties rather than establishing that the optimized engine computes the theorem’s verdicts at every token boundary. A slow reference evaluator built directly from the formal rules, enabling prefix-by-prefix correspondence testing against the shipped engine, is future work. False prunes. Over the 65 in-fragment valid programs of the cohort (40 ML, 25 C), the oracle was evaluated at every prefix and never reported Lost: 0/400/40 on ML and 0/250/25 on C, with Wilson 95% upper bounds of 8.8% and 13.3% (5.6% pooled). The bound is honest about cohort size, and extension is mechanical: add programs, rerun, diff every prefix. The recursion probe. 42 programs probing let rec corners agree with ocamlc in 42/42 cases (Wilson 95% CI [0.92,1.00][0.92,1.00]). The probe exists because recursion is where our fragment boundary was wrong once (§3.2): the harness that found the unsoundness now pins the repaired boundary. Prune lead time. On 30 invalid programs, the semantic oracle reports Lost mid-stream in 25 cases (12/17 on ML, 13/13 on C), where a syntax-only oracle catches 0 before end of input. In the caught cases the Lost position trails the start of the compiler’s diagnostic span by 2.3 characters pooled (2.5 on ML, 2.1 on C). Oracle cost. Median whole-input try_feed time on four synthetic stress families grows smoothly and mildly superlinearly with expression size, at log–log slopes of roughly 1.1–1.4 (Figure 3). The largest inputs, 450-token C declaration sequences and 65-application STLC chains, the adversarial case for chart size, stay under ∼130 130 ms. The measurement is model-free and CPU-only, on a six-core laptop CPU. 10010^010110^110210^210010^010110^110210^2Expression size (tokens)Median validation time (ms)Arithmetic flat sumArithmetic nestedC declarationsSTLC application chain Figure 3. Median validation time vs. expression size on four stress families (log–log). Growth is smooth and mildly superlinear (log–log slopes ≈1.1≈1.1–1.41.4).Log-log line chart of median validation time in milliseconds against expression size in tokens for four grammar families. All four curves are smooth and close to straight lines with slopes slightly above one. C declaration sequences reach 125 ms at 450 tokens and STLC application chains 131 ms at 65 tokens. 4.2. Constrained Generation Setup. We run twelve open models with full logit access: Qwen3.5 at 2B, 4B, and 9B in instruct and base variants, Qwen3.5-0.8B (instruct only), Qwen3.6-27B, Phi-4-mini, gpt-oss-20b, gemma-4-26b, and Pythia-1.4B (Biderman et al., 2023) as a no-instruction floor. The single-shot corpus is 52 tasks (33 STLC, 14 core ML, 5 C). The agentic corpus is tool episodes in three dialects. Each attempt runs in one of five decoding modes: • Unconstrained: free decoding, no mask. • Constrained Direct: the semantic mask on every token. • Constrained Mixed: free reasoning, then a constrained emission block, the interleaved schedule of CRANE (Banerjee et al., 2025). • Unconstrained Thinking: a budgeted chain-of-thought phase, then a free answer (Wei et al., 2022). • Syntactic Only: the same mask with the typing rules stripped, our within-framework ablation. Three models did not run Syntactic Only (Qwen3.6-27B, gemma-4-26b, gpt-oss-20b), so pooled comparisons are matched over the models that ran both modes being compared. Decoding is greedy at temperature 0, one attempt, fixed seed. Intervals are Wilson 95% and measure cohort uncertainty on hand-selected tasks, not population sampling. Grading is per-language and deliberately heterogeneous, and we do not pool it into one accuracy: • STLC: Aufbau supplies the decoding oracle and an independent handwritten validator checks the output type and β/α-equivalence against the reference. • tool: the executed return value against the registry’s real implementations. Behavioral. • ML: an output counts as valid only when Aufbau accepts the declared type and ocamlc independently accepts the program, and this program has the required type. • C: an output counts as valid only when Aufbau and c -fsyntax-only independently accept it. The divergence idiom that gives ML its coverage also inhabits any demanded type at grading time: of 259 passing ML records, 36 contain assert false (9 of the 52 passing direct-mask records). ocamlc’s independent check on the declared type is what keeps the ML criterion independent of the oracle. ML and C passes are therefore compiler-validated validity metrics rather than behavioral task-correctness metrics, and we reserve behavioral claims for STLC and tool. Each task is specified as a TOML file (prompt, initial prefix, reference program, resolution mode). Per-effect decomposition. Gains are heterogeneous across model classes. Across the nine models that ran both ablation arms, every observed semantic-minus-syntactic model–language point estimate was nonnegative. Constraint can repair weak and base models while taxing fluent ones: Qwen3.5-2B-Base rises from 0% unconstrained to 50% in mixed mode, while Qwen3.5-9B and Qwen3.6-27B both lose ground under the same mask. Mixed mode avoids the cost by confining the mask to a late emission block, tracking full chain-of-thought within a few points while emitting 28–36 tokens instead of 1,100–2,000. The semantic layer over syntax. The ablation isolates what the typing rules add over a pure CFG mask, holding parser, sampler, tokenizer bridge, and grammar fixed. This is the generation comparison the paper is about. The largest lifts by language are +15.2+15.2 points on STLC task correctness (Phi-4-mini) and +14.3+14.3 on ML validity (Qwen3.5-4B, Phi-4-mini, Qwen3.5-9B-Base), while every matched C cell is exactly 0. Aggregated within each language over the matched models, the semantic layer adds +7.1+7.1 points on ML (32.5% against 25.4%), +2.0+2.0 on STLC (40.4% against 38.4%), and exactly 0 on C (next paragraph). The ML figure carries the caveat that ML’s validity grader shares the oracle’s type system. Syntax-only constraining can itself hurt: pooled over models it sits below unconstrained on STLC (38.4%38.4\% against 44.4%44.4\%) and ML (25.4%25.4\% against 30.2%30.2\%), fighting the model’s prior with no semantic information to spend. That replicates, inside our own stack, the degradation CRANE (Banerjee et al., 2025) reports for constrain-from-the-first-token and the underperformance of grammar-only decoding in ChopChop’s tables (Nagy et al., 2026). PythiaQw-0.8BQw-2BQw-4BQw-9BPhi-4Qw-2B-BQw-4B-BQw-9B-B005510101515semantic −- syntactic (p)STLCML Figure 4. Per-model, per-language semantic-minus-syntactic difference in percentage points. STLC and ML are shown separately. C is omitted because every matched C difference is zero.Grouped bars show semantic-minus-syntactic pass-rate changes for nine models. All bars are nonnegative. The largest STLC increase is 15.2 points and the largest ML increases are 14.3 points. C is omitted because every matched change is zero. Where constraint helps, and a negative result. On the C-like fragment the direct mask lifts pooled validity from 53% to 80% (+27+27 points, matched over models that ran all five modes), but the syntax-only mask reaches the same 80%. The ablation attributes none of the C gain to the typing rules, and the difference is not significant. Format control alone explains the lift, and we report that as a negative result rather than crediting definition-before-use or pointer typing. These C cells were produced before the return-type check of §3.2 was added to c.auf, so they describe the earlier grammar. The added check tightens the semantic arm only, and rerunning the arm is future work. The semantic layer’s language-level gain concentrates on ML instead (+7.1+7.1 pooled), where inference-style typing constrains many surface choices. On STLC the direct mask is slightly negative pooled (44% to 40%) while mixed mode reaches 55%: those tasks are search-heavy rather than surface-heavy, so reasoning, not masking, binds. The tool dialects are the agentic case of §4.3. Uncons.Cons.Un. ThinkCons. Mix.002020404060608080100100Share of tasks (%)Observable final outcomes across decoding modessatisfied/passlost at stoplive at stopsatisfied/fail Figure 5. Observable final outcomes across 619 tasks and four decoding modes. Lost at stop: final verdict Lost. Live at stop: final verdict Live without a closed derivation. Satisfied/pass and /fail split closed outputs by the grader of §4.2. The labels are observable final states, with no inference about suffix existence, and the constrained arms carry no lost-at-stop mass and more live-at-stop mass.Four stacked bars show final outcomes for unconstrained, constrained direct, unconstrained thinking, and constrained mixed decoding. The two constrained modes have no Lost-at-stop mass and more Live-at-stop mass. Satisfied outputs are split into passing and failing outcomes. 4.3. Exploratory Observations Figure 6 shows the two rejection-telemetry observations. 0.8B2B4B9B27Bgpt-oss00112233445566pre-mask entropy (bits)(a) model uncertainty: entropy where the mask firestoken acceptedtoken rejected (retried)00252550507575100100ML syntaxML semanticC syntaxC semanticshare of positions (%)(b) grammar branching: tokens the oracle admits / positionforced (1)tight (2–4)open (5–16)wide (17+) Figure 6. (a) Mean pre-mask entropy at steps where the sampler’s first choice was accepted versus rejected (retried), per model, direct-mask arm: rejection is associated with the model’s uncertain steps. (b) Share of positions at which the oracle admits one candidate token (forced), a few (tight), or many, semantic oracle against syntactic-only (14 ML / 5 C programs). Two panels. Panel a is a grouped bar chart of pre-mask entropy in bits for six models. For each model the rejected-step bar is roughly twice the accepted-step bar or more. Panel b is a stacked horizontal bar chart with four rows, ML and C each under syntactic and semantic oracles, showing the distribution of admissible-set sizes binned as forced, tight, open, and wide. We see that semantic rows shift mass toward forced and tight bins. Rejection is associated with model uncertainty. Where the mask rejected the model’s first choice, pre-mask entropy is markedly higher than at accepted steps, at every scale of the Qwen instruct ladder: 0.87 against 1.71 bits at 0.8B, 0.94 against 1.67 at 2B, 0.53 against 1.06 at 4B, 0.37 against 1.28 at 9B, 0.22 against 0.81 at 27B, and 2.33 against 5.51 on gpt-oss-20b (Figure 6a). This is an association in single greedy runs, not a predictive evaluation, but it matches CRANE’s account of when constraint hurts (Banerjee et al., 2025): rejections concentrate at uncertain steps and are rare at confident ones. Retry pressure broadly falls with capability on that ladder (6.1% of steps at 0.8B, 2.1% at 27B, 13.9% on 2B-Base) but not across families, gpt-oss-20b retries 32.9%, while Pythia, the weakest model, retries only 6.8%, so this is not a model ranking. How strongly does the language constrain decoding? The rejection signal has a model-free counterpart: at each position of a valid program, how many candidate tokens does the oracle admit? We measure the mean log2 _2 admissible-set size over a corpus-derived token alphabet: a Hartley-style branching measure under a uniform assumption, not Shannon entropy, conditioned on the evaluated corpus (14 ML programs, 209 positions, 42-token alphabet, and 5 C programs, 83 positions). Over the ML corpus the semantic oracle admits 16.8 candidate tokens per position on average against 26.3 for its syntactic twin, removing 9.5 candidates per position and raising the share of forced positions, where exactly one candidate is legal, from 9% to 13% (Figure 6b). On C it admits 7.1 against 11.4. The typing layer thus closes roughly a third of the syntactic branching without ever rejecting the next gold token in the valid-corpus walk, and the measurement is model-free. 30301001003003001,0001,0003,0003,000Q3.5 0.8BQ3.5 2BQ3.5 4BQ3.5 9BQ3.6 27BPhi-4-minigpt-oss-20bmean generated tokensGeneration costthinkingmixed252550507575100100pass rate (%)Task performance Figure 7. Thinking vs. mixed mode: mean generated tokens on a log scale (left) and descriptive task-mix pass rate (right). Each row is one model and the line connects thinking (open purple) to mixed (filled orange). Mixed greatly reduces token count for the five Qwen rows (roughly 11×11× to 60×60×), but not for Phi-4-mini (0.73×0.73×, i.e. mixed emits more tokens) or gpt-oss-20b (1.14×1.14×). Pass-rate changes are heterogeneous across rows.Two aligned dot plots compare thinking and mixed decoding for seven models. Mixed uses far fewer tokens for five Qwen models, more for Phi-4-mini, and slightly fewer for gpt-oss-20b. Pass-rate changes vary by model. Agent episodes. Each turn decodes one registry step under the types established by prior turns, and episodes are graded by returned value. The comparison is unpaired (per-cell counts of 8 to 51), so we report direction only. Constrained Qwen3.5-4B-Base completes 57% of episodes (8/14) against 22% (4/18) unconstrained, while the fluent 4B is level (69% against 71%). Rates vary with surface form at least as much as with constraint: the fluent 4B reaches 88% on S-expressions against 50% on XML under the same typing rules. Several off-ladder models complete no episodes in either arm, and a paired design with matched coverage is future work. 5. Related Work Syntactic constrained decoding. Outlines compiles regular constraints to automata over the token vocabulary (Willard and Louf, 2023). PICARD prunes beam candidates by incremental parsing (Scholak et al., 2021), SynCode (Ugare et al., 2025b), Formatron (Sun et al., 2025), and DOMINO (Beurer-Kellner et al., 2024) optimize grammar-aligned masking to near-zero overhead, and subword alignment has a clean automaton treatment (Park et al., 2025). All decide membership in a fixed context-free or regular surface language. None carries the context-dependent state, such as scope, types, and declaration effects, on which models actually fail. Our syntactic layer uses the same Earley machinery. The contribution is the semantic layer above it and the contract analysis that survives the lift. Semantic constraints. ChopChop (Nagy et al., 2026) develops the general theory of semantic pruning for LLM decoding, casting admissibility as a realizability problem and stating soundness and completeness (their §3.4) relative to properties of the pruner the user programs: soundness needs an under-approximate or consistent checker, completeness an over-approximate and consistent one. For type safety they show no checker can be both, so their type pruner is over-approximate and consistent only to type depth three. We read their framework as the general setting our work instantiates. We use a declarative class with a context-free surface and decidable first-order semantic premises. Safe pruning follows from stable contradictions. Dead-end freedom is a separate grammar property for which we give sufficient productivity, type-coverage, and left-to-right-flow conditions (Theorem 2.6). The declarative route also gives a direct validation path: instances that check real languages can be tested prefix by prefix against production compilers (§4.1). Mündler et al. (Mündler et al., 2025) demonstrate type-constrained decoding for TypeScript with an incremental checker engineered for that language and evaluated at scale, a stronger per-language result than ours on its own territory. Our ML instance is a smaller monomorphic fragment, but comes from a declarative definition, and the same definition language yields the C-like fragment and the tool DSL with no new pruner code. IterGen (Ugare et al., 2025a) backtracks over partial generations to enforce per-symbol constraints and Synchromesh (Poesia et al., 2022) enforces per-domain checks. Neither analyzes the two prefix contracts separately. Tractable control via distillation into a tractable model (Zhang et al., 2023) enforces constraints by construction rather than by pruning, a complementary route. Grammar formalisms. The formalism assembles classical parts: attribute grammars with synthesized and inherited attributes (Knuth, 1968), definite-clause grammars, which showed unification against a logic program’s terms can carry a grammar’s semantics (Pereira and Warren, 1980), and unification-based grammar generally (Shieber, 1986). Semantic grammar specifications restrict these ideas to first-order terms, syntactic unification, and right-bound effects so that prefix verdicts are decidable and the pruning contract is analyzable. Condition (F) of §2.3 is the corresponding left-to-right restriction on a prefix parser. Differential testing. Validating a checker against an independent implementation is differential testing in McKeeman’s sense (McKeeman, 1998), and its randomized form found hundreds of bugs in production C compilers (Yang et al., 2011). Our variant tests prefix behavior: the compiler grades whole programs, the oracle grades every prefix, and the harness checks the two never disagree in the direction that matters for decoding. Reasoning and constraints. CRANE (Banerjee et al., 2025) establishes that constrained and unconstrained decoding are usefully interleaved, reasoning outside the constrained block, the answer inside it, and explains why constraining from the first token degrades reasoning. Our mixed mode is that architecture with a semantic rather than syntactic block, and the telemetry of §4.3 agrees with its account: rejection lands on exactly the uncertain steps. SynCode (Ugare et al., 2025b) reports the syntactic version. Editors, holes, incremental typing. Typing incomplete programs is an editor-services problem before it is a decoding problem. Hazel gives incomplete programs a semantics in which the unfilled position is a first-class typed hole (Omar et al., 2017). Our Pending binding is that object read through a parser, though Live is weaker than Hazel’s typing, saying only that no stable contradiction has appeared (§2.3). Incremental attribute evaluation with available/unavailable attributes goes back to Demers, Reps, and Teitelbaum (Demers et al., 1981). Merlin (Bour et al., 2018) is the engineering dual, recovering from broken text to keep services alive where we prune extensions of well-typed prefixes: recovery maximizes tolerance, pruning maximizes rejection, and both need the same incremental frontier. 6. Discussion and Limitations Formal limitations. The safe-pruning proof is a paper proof of Aufbau’s rejection discipline, not a mechanized proof of the code. Differential validation exercises the shipped implementation on finite cohorts, so implementation bugs outside those cohorts remain possible. Dead-end freedom is proved only for grammars satisfying the sufficient conditions of §2.3. We establish those conditions directly for the finite-lambda, core ML, and C-like fragments. We do not claim them for the tool DSLs, nor for the experimental STLC instance, whose unrestricted base-type universe defeats type coverage. The implementation does not attempt to infer this classification automatically. Token-sequence reachability is proved under exact spelling and the stated vocabulary-coverage hypothesis. Bounded proposal search additionally needs exhaustive masking, a deterministic fallback, or a separate sampler-fairness assumption which is assumed. Nothing is mechanized. Empirical limitations. The language metrics are heterogeneous: ML and C measure compiler-validated validity, STLC and tool tasks behavior. Generation uses one greedy attempt per task, the validation corpora are small and hand-selected, and the token-count and tool-episode comparisons are exploratory rather than causal. The C generation cells predate the return-type check now in c.auf (§3.2). 7. Conclusion A semantic prefix oracle owes the decoder two contracts, safe pruning and dead-end freedom. Aufbau provides safe pruning by rejecting only stable semantic contradictions. Dead-end freedom is separate. We give three sufficient grammar conditions, surface productivity, type coverage, and left-to-right constraint flow, and show how they separate the covered finite-lambda, ML, and C-like fragments from the uncovered experimental STLC and tool instances. A tokenizer-lifting lemma carries these guarantees from characters to token sequences under an explicit vocabulary-coverage hypothesis. Differential validation against production compilers shows zero false prunes across every prefix of 65 compiler-valid programs, and 25/30 invalid programs caught mid-stream where a syntax-only oracle catches none. These are finite compatibility results for the shipped engine, not an exhaustive correctness proof. In generation the matched ablation attributes positive observed lift to the typing rules on ML, while every matched C difference was zero, which format control alone can explain. The next steps are behavioral ML and C grading, generation experiments on the covered finite-lambda instance, a matched mixed-mode rerun, broader differential corpora, and mechanization. References Banerjee et al. (2025) D. Banerjee, T. Suresh, S. Ugare, S. Misailovic, and G. Singh CRANE: reasoning with constrained LLM generation. In Proceedings of the 42nd International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 267, p. 2836–2857. External Links: Link Cited by: 3rd item, §4.2, §4.3, §5. Beurer-Kellner et al. (2024) L. Beurer-Kellner, M. Fischer, and M. Vechev Guiding LLMs the right way: fast, non-invasive constrained generation. In Proceedings of the 41st International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 235, p. 3658–3673. External Links: Link Cited by: §1, §5. Biderman et al. (2023) S. Biderman, H. Schoelkopf, Q. G. Anthony, H. Bradley, K. O’Brien, E. Hallahan, M. A. Khan, S. Purohit, U. S. Prashanth, E. Raff, A. Skowron, L. Sutawika, and O. Van Der Wal Pythia: a suite for analyzing large language models across training and scaling. In Proceedings of the 40th International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 202, p. 2397–2430. External Links: Link Cited by: §4.2. Bour et al. (2018) F. Bour, T. Refis, and G. Scherer Merlin: a language server for OCaml (experience report). Proceedings of the ACM on Programming Languages 2 (ICFP), p. 103:1–103:15. External Links: Document Cited by: §5. Brzozowski (1964) J. A. Brzozowski Derivatives of regular expressions. Journal of the ACM 11 (4), p. 481–494. External Links: Document Cited by: §2.1. Demers et al. (1981) A. J. Demers, T. Reps, and T. Teitelbaum Incremental evaluation for attribute grammars with application to syntax-directed editors. In Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 105–116. External Links: Document Cited by: §2.2, §5. Earley (1970) J. Earley An efficient context-free parsing algorithm. Communications of the ACM 13 (2), p. 94–102. External Links: Document Cited by: §3.1. Knuth (1968) D. E. Knuth Semantics of context-free languages. Mathematical Systems Theory 2 (2), p. 127–145. External Links: Document Cited by: §5. Martelli and Montanari (1982) A. Martelli and U. Montanari An efficient unification algorithm. ACM Transactions on Programming Languages and Systems 4 (2), p. 258–282. External Links: Document Cited by: §2.2. McKeeman (1998) W. M. McKeeman Differential testing for software. Digital Technical Journal 10 (1), p. 100–107. Cited by: §5. Mündler et al. (2025) N. Mündler, J. He, H. Wang, K. Sen, D. Song, and M. Vechev Type-constrained code generation with language models. Proceedings of the ACM on Programming Languages 9 (PLDI), p. 601–626. External Links: Document Cited by: §5. Nagy et al. (2026) S. Nagy, T. Zhou, N. Polikarpova, and L. D’Antoni ChopChop: a programmable framework for semantically constraining the output of language models. Proceedings of the ACM on Programming Languages 10 (POPL), p. 1905–1932. External Links: Document Cited by: §4.2, §5. Omar et al. (2017) C. Omar, I. Voysey, M. Hilton, J. Aldrich, and M. A. Hammer Hazelnut: a bidirectionally typed structure editor calculus. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, p. 86–99. External Links: Document Cited by: §2.2, §5. Owens et al. (2009) S. Owens, J. Reppy, and A. Turon Regular-expression derivatives re-examined. Journal of Functional Programming 19 (2), p. 173–190. External Links: Document Cited by: §2.1. Park et al. (2025) K. Park, T. Zhou, and L. D’Antoni Flexible and efficient grammar-constrained decoding. In Proceedings of the 42nd International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 267, p. 48262–48275. External Links: Link Cited by: §5. Pereira and Warren (1980) F. C. N. Pereira and D. H. D. Warren Definite clause grammars for language analysis—a survey of the formalism and a comparison with augmented transition networks. Artificial Intelligence 13 (3), p. 231–278. External Links: Document Cited by: §5. Poesia et al. (2022) G. Poesia, A. Polozov, V. Le, A. Tiwari, G. Soares, C. Meek, and S. Gulwani Synchromesh: reliable code generation from pre-trained language models. In International Conference on Learning Representations, External Links: Link Cited by: §5. Robinson (1965) J. A. Robinson A machine-oriented logic based on the resolution principle. Journal of the ACM 12 (1), p. 23–41. External Links: Document Cited by: §2.2. Scholak et al. (2021) T. Scholak, N. Schucher, and D. Bahdanau PICARD: parsing incrementally for constrained auto-regressive decoding from language models. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, p. 9895–9901. External Links: Document, Link Cited by: §5. Shieber (1986) S. M. Shieber An introduction to unification-based approaches to grammar. CSLI Lecture Notes, CSLI Publications, Stanford, CA. Cited by: §5. Sun et al. (2025) X. Sun, C. Wei, M. Tian, and S. Ni Earley-driven dynamic pruning for efficient structured decoding. In Proceedings of the 42nd International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 267, p. 57773–57789. External Links: Link Cited by: §1, §5. Ugare et al. (2025a) S. D. Ugare, R. Gumaste, T. Suresh, G. Singh, and S. Misailovic IterGen: iterative semantic-aware structured LLM generation with backtracking. In The Thirteenth International Conference on Learning Representations, External Links: Link Cited by: §5. Ugare et al. (2025b) S. Ugare, T. Suresh, H. Kang, S. Misailovic, and G. Singh SynCode: LLM generation with grammar augmentation. Transactions on Machine Learning Research. External Links: ISSN 2835-8856, Link Cited by: §5, §5. Wei et al. (2022) J. Wei, X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. Chi, Q. V. Le, and D. Zhou Chain-of-thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems, Vol. 35, p. 24824–24837. External Links: Link Cited by: 4th item. Willard and Louf (2023) B. T. Willard and R. Louf Efficient guided generation for large language models. External Links: 2307.09702, Document, Link Cited by: §1, §5. Yang et al. (2011) X. Yang, Y. Chen, E. Eide, and J. Regehr Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, p. 283–294. External Links: Document Cited by: §5. Zhang et al. (2023) H. Zhang, M. Dang, N. Peng, and G. Van Den Broeck Tractable control for autoregressive language generation. In Proceedings of the 40th International Conference on Machine Learning, Proceedings of Machine Learning Research, Vol. 202, p. 40932–40945. External Links: Link Cited by: §5.