Static typing for a substructural lambda calculus

摘要

Substructural type systems are designed from the insight inspired by the development of linear and substructural logics. Substructural type systems promise to control the usage of computational resources statically, thus detect more program errors at an early stage than traditional type systems do. In the past decade, substructural type systems have been deployed in the design of novel programming languages, such as Vault, etc. This paper presents a general typing theory for substructural type system. First, we define a universal semantic framework for substructural types by interpreting them as characteristic intervals composed of type qualifiers. Based on this framework, we present the design of a substructural calculus λSL with subtyping relations. After giving syntax, typing rules and operational semantics for λSL, we prove the type safety theorem. The new calculus λSL can guarantee many more safety invariants than traditional lambda calculus, which is demonstrated by showing that the λSL calculus can serve as an idealized type intermediate language, and defining a type-preserving translation from ordinary typed lambda calculus into λSL.