[Submitted on 11 Sep 2026 (this version), latest revision 18 Sep 2026 (v6)]
Title:The LeanExe Subset: Types, Extraction, and Execution
Abstract: LeanExe compiles checked Lean declarations to WebAssembly through a restricted first-order extraction path. The LeanExe subset is specified here by runtime typing and layout rules together with an implementation-indexed relation from checked declarations to WebAssembly execution. The report separates kernel typing, static specialization, extraction acceptance, ownership analysis, binary validity, and artifact behavior. It defines the internal and public type domains, proves two layout propositions, and states the numeric, collection, memory, and fixed-adapter semantics, including binary32 arithmetic and packed word storage. It also states the proof obligation for checking a compilation against its Lean algorithm. A source audit identifies incomplete runtime export-name rejection and a child-mask width obligation. The reference IR evaluator has a narrower comparison domain than compiled execution. Existing emitter, decoder, validator, packed-memory, and arithmetic theorems support their named boundaries. An independent source operational semantics, mechanized acceptance judgments, and a general source-to-WebAssembly refinement theorem remain open.
| Comments: | 16 pages |
| Subjects: | Programming Languages (cs.PL); Logic in Computer Science (cs.LO) |
| Cite as: | marXiv:2609.00005 [cs.PL] (or marXiv:2609.00005v1 [cs.PL] for this version) |
Submission history
[v1] Fri, 11 Sep 2026 16:32:04 UTC (346 KB)
[v2] Fri, 11 Sep 2026 16:38:03 UTC (346 KB)
[v3] Fri, 18 Sep 2026 16:17:22 UTC (362 KB)
[v4] Fri, 18 Sep 2026 16:22:01 UTC (362 KB)
[v5] Fri, 18 Sep 2026 16:30:32 UTC (363 KB)
[v6] Fri, 18 Sep 2026 16:35:44 UTC (363 KB)
Named by
- marXiv:2609.00014
- Applies the LeanExe compilation and verification approach described here.
- marXiv:2609.00011
- Applies the per-compilation correspondence method to cached GPT-2 inference with packed FP32 runtime weights.