Static Overload Resolution and Monomorphization for Functional Languages

We present a formal framework for the static resolution of function overloading in an extension of the simply typed lambda-calculus, coupled with a construction relation via global monomorphization. Our system reconciles the flexibility of local extension declarations with a deterministic selection of the most specific implementation, structurally eliminating the resolution indirection associated with passing dictionaries or dispatch tables. We formalize the syntax, the declarative type system, and the specialization semantics of this calculus, and we establish mechanized metatheoretical guarantees in Coq/Rocq: type uniqueness, type preservation under elaboration, forward semantic simulation, and the End-to-End Soundness theorem.