Title: Typing Strictness (Extended Version) Show Chinese title

Title: 严格性输入（扩展版）

Abstract: 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. Show Chinese abstract

Abstract: 严格性分析对于具有非严格求值的语言的高效实现至关重要，可以减轻惰性带来的大部分性能开销。 然而，在源代码级别进行严格性推理可能具有挑战性且不直观。 我们提出了一种新的严格性定义，通过更精确地描述变量使用来改进传统的定义。 我们在按名调用和按推值调用设置中为该定义建立了类型理论基础，受到跟踪效果和协效果类型系统文献的启发。 我们通过逻辑关系证明了我们的类型系统计算出的严格性属性准确描述了运行时变量的使用，并提供了从按名调用系统到按推值调用系统的保持严格性注解的翻译。 我们所有的结果都在Rocq中进行了形式化。