Abstract We introduce a geometric model of shallow multiplicative exponential linear logic (MELL) using the Hilbert scheme. Building on previous work interpreting multiplicative linear logic (MLL) proofs as systems of linear equations, we show that shallow MELL proofs can be modelled by locally projective schemes. The key insight is that while MLL proofs correspond to equations between formulas, the exponential fragment of shallow proofs corresponds to equations between these equations. We prove that the model is invariant under cut-elimination by constructing explicit isomorphisms between the schemes associated with proofs related by cut-reduction steps. A key technical tool is the interpretation of the exponential modality using the Hilbert scheme, which parameterises closed subschemes of projective space. We demonstrate the model through detailed examples, including an analysis of Church numerals that reveals how the Hilbert scheme captures the geometric content of promoted formulas. This work establishes new connections between proof theory and algebraic geometry, suggesting broader relationships between computation and scheme theory.

Abstract The Curry–Howard correspondence is often described as relating proofs (in intuitionistic natural deduction) to programs (terms in simply-typed lambda calculus). However, this narrative is hardly a perfect fit, due to the computational content of cut-elimination and the logical origins of the lambda calculus. We revisit Howard’s work and interpret it as an isomorphism between a category of formulas and proofs in intuitionistic sequent calculus and a category of types and terms in simply-typed lambda calculus. In our telling of the story, the fundamental duality is not between proofs and programs but between emphlocal (sequent calculus) and global (lambda calculus or natural deduction) points of view on a common logico-computational mathematical structure.