一句话：提出更精细的严格性定义，并在按名调用与 CBPV 中建立类型系统，证明其准确刻画变量的运行时使用。
严格性分析对非严格语言的性能至关重要，但在源代码层面推理严格性困难且不直观，传统定义对变量使用的描述也不够精确。本文提出一种细化的严格性定义，借鉴效应与余效应类型系统的思想，在按名调用（call-by-name）和按值调用推值（call-by-push-value）两种设定下建立类型论基础。通过逻辑关系证明，类型系统计算出的严格性属性能够准确描述变量在运行时的使用情况，并给出从 call-by-name 到 call-by-push-value 的保持严格性标注的翻译。所有结果均已在 Rocq 中机器化验证。
Strictness analysis is critical to efficient implementation of languages with non-strict evaluation, mitigating much of the performance overhead of laziness. However, reasoning about strictness at the source level can be challenging and unintuitive. We propose a new definition of strictness that refines the traditional one by describing variable usage more precisely. We lay type-theoretic foundations for this definition in both call-by-name and call-by-push-value settings, drawing inspiration from the literature on type systems tracking effects and coeffects. We prove via a logical relation that the strictness attributes computed by our type systems accurately describe the use of variables at runtime, and we offer a strictness-annotation-preserving translation from the call-by-name system to the call-by-push-value one. All our results are mechanized in Rocq.
@article{SainatiCPW26,
title = {Typing Strictness},
author = {Daniel Sainati and Joseph W. Cutler and Benjamin C. Pierce and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776657}
}