一句话：提出一种强 call-by-need 求值策略，可计算开放 λ 项的强范式，并用非幂等交类型证明其完备性。
论文研究开放 λ 项的强范式计算：归约可进入抽象体与替换内部，项也可含自由变量。作者提出一种强 call-by-need 求值策略，保证参数仅在需要时求值且至多一次。为证明完备性，他们定义可在任意上下文归约的强 call-by-need 演算，并采用非幂等交类型：纯 λ 演算中具有 β-强范式的项可被类型化，可类型化蕴含该演算的弱规范化，而弱规范化又蕴含强 call-by-need 策略的规范化。由此该策略对归约到 β-强范式完备，并被证明保守扩展标准弱 call-by-need。
We present a call-by-need strategy for computing strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), which guarantees that arguments are only evaluated when needed and at most once. The strategy is shown to be complete with respect toβ-reduction to strong normal form. The proof of completeness relies on two key tools: (1) the definition of a strong call-by-need calculus where reduction may be performed inside any context, and (2) the use of non-idempotent intersection types. More precisely, terms admitting aβ-normal form in pure lambda calculus are typable, typability implies (weak) normalisation in the strong call-by-need calculus, and weak normalisation in the strong call-by-need calculus implies normalisation in the strong call-by-need strategy. Our (strong) call-by-need strategy is also shown to be conservative over the standard (weak) call-by-need.
@article{BalabonskiBBK17,
title = {Foundations of strong call by need},
author = {Thibaut Balabonski and Pablo Barenbaum and Eduardo Bonelli and Delia Kesner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110264}
}