{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:14:13Z","timestamp":1784211253663,"version":"3.55.0"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"National Science Foundation","award":["2313998"],"award-info":[{"award-number":["2313998"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2402449"],"award-info":[{"award-number":["2402449"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3776657","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"413-443","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Typing Strictness"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-4738-8524","authenticated-orcid":false,"given":"Daniel","family":"Sainati","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9399-9308","authenticated-orcid":false,"given":"Joseph W.","family":"Cutler","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7839-1636","authenticated-orcid":false,"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Andreas Abel and Jean-Philippe Bernardy. 2020. A unified view of modalities in type systems. 4 (2020) 1\u201328. Issue ICFP. doi:10.1145\/3408972","DOI":"10.1145\/3408972"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_2_4_2","unstructured":"Erik Barendsen and Sjaak Smetsers. 2007. Strictness Analysis via Resource Typing. https:\/\/www.cs.ru.nl\/barendregt60\/essays\/barendsen_smetsers\/art02_barendsen_smetsers.pdf"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622843"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99382"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804308"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Pritam Choudhury Harley Eades III Richard A. Eisenberg and Stephanie Weirich. 2021. A graded dependent type system with a usage-aware semantics. 5 (2021) 1\u201332. Issue POPL. doi:10.1145\/3434331","DOI":"10.1145\/3434331"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.2307\/1968337"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498692"},{"key":"e_1_3_2_15_2","unstructured":"Edkso de Vries. 2017. Visualizing lazy evaluation. https:\/\/www.well-typed.com\/blog\/2017\/09\/visualize-cbn\/"},{"key":"e_1_3_2_16_2","unstructured":"Edkso de Vries. 2020. Being lazy without getting bloated. https:\/\/well-typed.com\/blog\/2020\/09\/nothunks\/"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408986"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/944746.944731"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3359619.3359744"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294097"},{"key":"e_1_3_2_22_2","unstructured":"The R Foundation. 1999. https:\/\/www.r-project.org\/"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360579"},{"key":"e_1_3_2_27_2","unstructured":"Haskell.org. 1996. The Glasgow Haskell Compiler. https:\/\/www.haskell.org\/ghc\/"},{"key":"e_1_3_2_28_2","unstructured":"Haskell.org. 1996. Haskell Language. https:\/\/www.haskell.org\/"},{"key":"e_1_3_2_29_2","unstructured":"HaskellWiki. 2019. Foldr Foldl Foldl\u2019. https:\/\/wiki.haskell.org\/Foldr_Foldl_Foldl\u2019"},{"key":"e_1_3_2_30_2","unstructured":"HaskellWiki. 2021. Weak head normal form. https:\/\/wiki.haskell.org\/Weak_head_normal_form"},{"key":"e_1_3_2_31_2","unstructured":"HaskellWiki. 2022. Performance\/Strictness. https:\/\/wiki.haskell.org\/Performance\/Strictness"},{"key":"e_1_3_2_32_2","unstructured":"HaskellWiki. 2025. seq. https:\/\/wiki.haskell.org\/index.php?title=Seq"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236783"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/648332.755572"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964010"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103698"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535846"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371083"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729324"},{"key":"e_1_3_2_41_2","unstructured":"Steve Klabnik Carol Nichols and Chris Krycho. 2024. Processing a Series of Items with Iterators. https:\/\/doc.rust-lang.org\/book\/ch13-02-iterators.html#processing-a-series-of-items-with-iterators"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3196-0_17"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41638"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99390"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001878"},{"key":"e_1_3_2_47_2","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2025. https:\/\/ocaml.org\/manual\/5.3\/api\/Lazy.html"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_17"},{"key":"e_1_3_2_49_2","unstructured":"Paul Blain Levy. 2001. Call-By-Push-Value. https:\/\/qmro.qmul.ac.uk\/xmlui\/handle\/123456789\/4742"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0954-6"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"Paul Blain Levy. 2006. Call-by-push-value: Decomposing call-by-value and call-by-name. 19 4 (2006) 377\u2013414. doi:10.1007\/s10990-006-0480-6","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3537668.3537670"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00022-2"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Dylan McDermott. 2025. Grading call-by-push-value explicitly and implicitly. doi:10.4230\/LIPIcs.FSCD.2025.25","DOI":"10.4230\/LIPIcs.FSCD.2025.25"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1515\/comp-2018-0009"},{"key":"e_1_3_2_57_2","doi-asserted-by":"crossref","unstructured":"Dylan McDermott and Alan Mycroft. 2019. Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order.. In ESOP. 235\u2013262.","DOI":"10.1007\/978-3-030-17184-1_9"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763143"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"Henry Mercer Cameron Ramsay and Neel Krishnaswami. 2022. Implicit Polarized F: local type inference for impredicativity. (03 2022). doi:10.48550\/arXiv.2203.01835","DOI":"10.48550\/arXiv.2203.01835"},{"key":"e_1_3_2_60_2","unstructured":"Neil Mitchell. 2013. Destroying Performance with Strictness. https:\/\/neilmitchell.blogspot.com\/2013\/08\/destroying-performance-with-strictness.html"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.5555\/647324.721526"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888271"},{"key":"e_1_3_2_63_2","unstructured":"Max S. New. 2023. Compiling with Call-by-push-value. (2023). https:\/\/maxsnew.com\/docs\/mfps2023-slides.pdf"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/210184.210187"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_35"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628160"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","unstructured":"Pierre-Marie P\u00e9drot and Nicolas Tabareau. 2019. The fire triangle: how to mix substitution dependent elimination and effects. 4 (2019) 1\u201328. Issue POPL. doi:10.1145\/3371126","DOI":"10.1145\/3371126"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863568"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","unstructured":"Nick Rioux and Steve Zdancewic. 2020. Computation focusing. 4 (2020) 95:1\u201395:27. Issue ICFP. doi:10.1145\/3408977","DOI":"10.1145\/3408977"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_13"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","unstructured":"Daniel Sainati Joseph W. Cutler Benjamin C. Pierce and Stephanie Weirich. 2025. Artifact associated with \"Typing Strictness\". doi:10.5281\/zenodo.17279039","DOI":"10.5281\/zenodo.17279039"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","unstructured":"Daniel Sainati Joseph W. Cutler Benjamin C. Pierce and Stephanie Weirich. 2025. Typing Strictness (Extended Version). doi:10.48550\/arXiv.2510.16133","DOI":"10.48550\/arXiv.2510.16133"},{"key":"e_1_3_2_74_2","unstructured":"Typelevel Scala. 2013. FS2: Functional effectful concurrent streams for Scala. https:\/\/fs2.io\/#\/"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_27"},{"key":"e_1_3_2_76_2","unstructured":"Ilya Sergey Simon Peyton Jones and Dimitrios Vytiniotis. 2014. Theory and practice of demand analysis in Haskell. (2014). https:\/\/www.microsoft.com\/en-us\/research\/publication\/theory-practice-demand-analysis-haskell\/"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535861"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40447-4_6"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","unstructured":"J.-P. Talpin and P. Jouvelot. 1992. The type and effect discipline. In [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (1992-06). 162\u2013173. doi:10.1109\/LICS.1992.185530","DOI":"10.1109\/LICS.1992.185530"},{"key":"e_1_3_2_80_2","unstructured":"Rocq Team. 2025. The Rocq Prover. https:\/\/rocq-prover.org\/"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","unstructured":"Cassia Torczon Emmanuel Su\u00e1rez Acevedo Shubh Agrawal Joey Velez-Ginorio and Stephanie Weirich. 2024. Effects and Coeffects in Call-by-Push-Value. 8 (2024) 1108\u20131134. Issue OOPSLA2. doi:10.1145\/3689750","DOI":"10.1145\/3689750"},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224168"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","unstructured":"Marco Vassena Joachim Breitner and Alejandro Russo. 2017. Securing Concurrent Lazy Programs Against Information Leakage. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 37\u201352. doi:10.1109\/CSF.2017.39","DOI":"10.1109\/CSF.2017.39"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_3_2_85_2","unstructured":"Philip Wadler. 1987. Strictness analysis on non-\ufb02at domains (by abstract interpretation over finite domains). In Abstract Interpretation of Declarative Languages. Halsted Press."},{"key":"e_1_3_2_86_2","unstructured":"Philip Wadler. 1993. Linear Types Can Change the World! (10 1993)."},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.5555\/645419.652502"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"},{"key":"e_1_3_2_89_2","volume-title":"Semantics and Pragmatics of the Lambda-calculus","author":"Wadsworth C.P.","year":"1971","unstructured":"C.P. Wadsworth. 1971. Semantics and Pragmatics of the Lambda-calculus. University of Oxford. https:\/\/books.google.com\/books?id=kl1QIQAACAAJ"},{"key":"e_1_3_2_90_2","doi-asserted-by":"publisher","DOI":"10.48456\/tr-623"},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292545"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674626"},{"key":"e_1_3_2_93_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_4"},{"key":"e_1_3_2_94_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020843229247"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776657","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:39:56Z","timestamp":1784209196000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776657"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":93,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776657"],"URL":"https:\/\/doi.org\/10.1145\/3776657","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}