Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together without making use of an encoding into a common target framework. This work proposes an intersection type system for PCF with a specific notion of evaluation, called PCFH. Evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV-like operational behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the reduction sequences to normal form. This type system is then refined to a tight one, offering exact information regarding the length of normalization sequences. This is the first time that a sound and complete quantitative type system has been designed for a hybrid computational model.

翻译：交集类型系统已被独立应用于不同的求值策略，例如按名调用（CBN）和按值调用（CBV）。这些类型系统随后被推广到不同的包含性范式，特别地，能够在一个统一的框架中对CBN和CBV进行编码。然而，目前尚不存在能显式地让CBN和CBV共存而无需将其编码为共同目标的交集类型系统。本文针对带有特定求值概念PCFH的PCF语言提出了一种交集类型系统。PCFH中的求值实际上具有混合性质，即CBN和CBV的操作行为共存：PCFH对函数应用采用类似CBV的操作行为，而对递归采用类似CBN的行为。这种混合性质体现在类型系统中，该类型系统对PCFH是可靠且完备的：不仅可类型化蕴含可规范化，反之亦然。此外，该类型系统是定量的，即类型推演的大小为归约序列到范式的长度提供了上界。该类型系统随后被精炼为紧致类型系统，能够提供关于规范化序列长度的精确信息。这是首次为混合计算模型设计出可靠且完备的定量类型系统。