Static Typing with Value Space-based Subtyping

This paper presents a formal type system for atomic value types as an extension of the simply typed lambda calculus with subtyping. In the λ_C-calculus, value types can be derived through the application of value space constraints.