2025/10/17 by Daniel Sainati, Sainati, Daniel, Joseph W. Cutler +5 · 1 voice
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering Research #cs.PL
paper · pdf · doi:10.48550/arxiv.2510.16133
openalex publication_date 2025/10/17 · arxiv published 2025/10/17 · openalex created_date 2025/10/22 · arxiv updated 2026/01/08 · openalex updated_date 2026/07/28
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.