出版社：Academy & Industry Research Collaboration Center (AIRCC)
摘要：The operation of substitution in 𝜆-calculus is treated as an atomic operation. It makes that
substitution operation is complex to be analyzed. To overcome this drawback, explicit
substitution systems are proposed. They bridge the gap between the theory of the 𝜆-calculus and
its implementation in programming languages and proof assistants. 𝜆𝑜-calculus is a name-free
explicit substitution. Intersection type systems for various explicit substitution calculi, not
including λo-calculus, have been studied by researchers. In this paper, we put our attention to
𝜆𝑜-calculus. We present an intersection type system for 𝜆𝑜-calculus and show it satisfies the
subject reduction property.
关键词：Intersection type; Lambda calculus; Director strings; Subject reduction
