Linking as Evaluation: Correct Separate Compilation via First-Class Environments
Jam Kabeer Ali Khan, Jinhao Tan, Bruno C. d. S. Oliveira
cs.PL
Nov 3, 2026 · v1
TL;DR
All metatheory of the λ_SCE calculus, including type safety, elaboration and separate compilation correctness, is mechanized in Lean 4.
Abstract
Separate compilation is central to modular software: components are compiled independently and linked into an executable. Separate compilation is correct when a linked program behaves like the program formed by merging its sources. This property is less routine to prove than type soundness because it requires a formal account of linking. We present $λ_{\mathsf{SCE}}$, a simply typed calculus in which linking, modules, and environments are all first-class. Programmers control module linking through a link operator, which a type-directed elaboration translates into ordinary terms of a core calculus of first-class environments. The core calculus's existing evaluation rules then perform the linking: linking as evaluation. Linking independently compiled modules yields the same core term as elaborating their source link. Therefore, compilation and linking commute by construction. As a result, separate compilation correctness follows directly from the semantics preservation for both static and dynamic linking. All meta-theory is mechanized in Lean 4, and we implement a compiler to WebAssembly in OCaml.
Problem
Separate compilation is correct when linking independently compiled components behaves like linking their sources. Proving this requires a formal account of linking, and prior typed calculi either link outside the language or lack such a proof, especially for dynamic linking.
Approach
The authors introduce λ_SCE, a simply typed calculus with first-class modules, environments, and a link operator. A type-directed elaboration translates it into λ_E, a core calculus of first-class environments with dependent merges. The core calculus's evaluation rules then perform linking ('linking as evaluation'), so compilation and linking commute by construction. The calculus is extended with unions, iso-recursive types, fixpoints and multi-import linking, and a WebAssembly compiler is implemented in OCaml.
Results
Separate compilation correctness follows from semantics and behavior preservation for both static and dynamic linking. Type safety, interface abstraction and all extensions are proved, and every proof is checked in Lean 4.
