Serhii Glova

One Integer for Semantic Work and Materialization: A Mechanized, Content-Addressed Combinator Machine over Term, Budget and Content Environment, and the Engineering of Trustworthy Proof Artifacts

We present Σ-GLYPH Book I, a content-addressed combinator machine in which a single unsigned integer budget — ATP — prices both the semantic work an evaluation performs and the peak number of nodes it materializes, and we report a layered Lean 4 mechanization of it. Three framing...

One Integer for Work and Memory: A Mechanized, Content-Addressed Combinator Machine, and the Engineering of Trustworthy Proof Artifacts

We present Σ-GLYPH Book I, a content-addressed combinator machine in which a single unsigned integer budget — *ATP* — prices both the work an evaluation performs and the *peak* memory it materializes, and we report a layered Lean 4 mechanization of it. The central theorem, `EvalM...