{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:56:11Z","timestamp":1776891371927,"version":"3.51.2"},"reference-count":54,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"4","license":[{"start":{"date-parts":[[2007,11,8]],"date-time":"2007-11-08T00:00:00Z","timestamp":1194480000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This paper proves correctness of N\u00f6cker's method of strictness analysis, implemented in the Clean compiler, which is an effective way for strictness analysis in lazy functional languages based on their operational semantics. We improve upon the work Clark, Hankin and Hunt did on the correctness of the abstract reduction rules in two aspects. Our correctness proof is based on a functional core language and a contextual semantics, thus proving a wider range of strictness-based optimizations as correct, and our method fully considers the cycle detection rules, which contribute to the strength of N\u00f6cker's strictness analysis.<\/jats:p>\n                  <jats:p>\n                    Our algorithm SAL is a reformulation of N\u00f6cker's strictness analysis algorithm in a functional core language LR. This is a higher order call-by-need lambda calculus with\n                    <jats:monospace>case<\/jats:monospace>\n                    , constructors,\n                    <jats:monospace>letrec<\/jats:monospace>\n                    , and\n                    <jats:monospace>seq<\/jats:monospace>\n                    , which is extended during strictness analysis by set constants like\n                    <jats:monospace>Top<\/jats:monospace>\n                    or\n                    <jats:italic>Inf<\/jats:italic>\n                    , denoting sets of expressions, which indicate different evaluation demands. It is also possible to define new set constants by recursive equations with a greatest fixpoint semantics. The operational semantics of LR is a small-step semantics. Equality of expressions is defined by a contextual semantics that observes termination of expressions. Basically, SAL is a nontermination checker. The proof of its correctness and hence of N\u00f6cker's strictness analysis is based mainly on an exact analysis of the lengths of evaluations, i.e., normal-order reduction sequences to WHNF. The main measure being the number of \u201cessential\u201d reductions in evaluations.\n                  <\/jats:p>\n                  <jats:p>Our tools and results provide new insights into call-by-need lambda calculi, the role of sharing in functional programming languages, and into strictness analysis in general. The correctness result provides a foundation for N\u00f6cker's strictness analysis in Clean, and also for its use in Haskell.<\/jats:p>","DOI":"10.1017\/s0956796807006624","type":"journal-article","created":{"date-parts":[[2007,11,8]],"date-time":"2007-11-08T06:50:00Z","timestamp":1194504600000},"page":"503-551","source":"Crossref","is-referenced-by-count":23,"title":["Safety of N\u00f6cker's strictness analysis"],"prefix":"10.46298","volume":"18","author":[{"given":"MANFRED","family":"SCHMIDT-SCHAUSS","sequence":"first","affiliation":[]},{"given":"DAVID","family":"SABEL","sequence":"additional","affiliation":[]},{"given":"MARKO","family":"SCH\u00dcTZ","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2007,11,8]]},"reference":[{"key":"S0956796807006624_manual_ref-33","volume-title":"Haskell 98 Language and Libraries.","author":"Peyton","year":"2003"},{"key":"S0956796807006624_manual_ref-42","unstructured":"Santos, A. (1995) Compilation by Transformation in Non-Strict Functional Languages. Ph.D. thesis, University of Glasgow."},{"key":"S0956796807006624_manual_ref-14","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"S0956796807006624_manual_ref-32","volume-title":"Static Analysis Symposium","author":"Paterson","year":"1996"},{"key":"S0956796807006624_manual_ref-8","first-page":"42","volume-title":"Programs as Data Structures.","author":"Burn","year":"1985"},{"key":"S0956796807006624_manual_ref-16","first-page":"78","volume-title":"Functional programming, Glasgow 1994.","author":"Gordon","year":"1994"},{"key":"S0956796807006624_manual_ref-48","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2007010"},{"key":"S0956796807006624_manual_ref-5","first-page":"233","volume-title":"Principles of Programming Languages.","author":"Ariola","year":"1995"},{"key":"S0956796807006624_manual_ref-49","unstructured":"Sch\u00fctz, M. (1994) Striktheits-Analyse mittels abstrakter Reduktion f\u00fcr den Sprachkern einer nicht-strikten funktionalen Programmiersprache. Diploma thesis, Johann Wolfgang Goethe-Universit\u00e4t, Frankfurt."},{"key":"S0956796807006624_manual_ref-51","volume-title":"Term Graph Rewriting - Theory and Practice","author":"van","year":"1993"},{"key":"S0956796807006624_manual_ref-19","first-page":"260","volume-title":"Functional Programming Languages and Computer Architecture.","author":"Kuo","year":"1989"},{"key":"S0956796807006624_manual_ref-15","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00043-3"},{"key":"S0956796807006624_manual_ref-30","first-page":"155","volume-title":"Implementation of Functional Languages (IFL '98) London","author":"Pape","year":"1998"},{"key":"S0956796807006624_manual_ref-52","volume-title":"Abstract interpretation of declarative languages","author":"Wadler","year":"1987"},{"key":"S0956796807006624_manual_ref-7","volume-title":"The Lambda Calculus. Its Syntax and Semantics.","author":"Barendregt","year":"1984"},{"key":"S0956796807006624_manual_ref-4","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00185-L"},{"key":"S0956796807006624_manual_ref-20","first-page":"293","article-title":"State in Haskell","volume":"8","author":"Launchbury","year":"1995","journal-title":"LISP Symb. Comput."},{"key":"S0956796807006624_manual_ref-31","unstructured":"Pape, Dirk. (2000) Striktheitsanalysen funktionaler Sprachen. Ph.D. thesis, Fachbereich Mathematik und Informatik, Freie Universit\u00e4t Berlin. (in German.)"},{"key":"S0956796807006624_manual_ref-38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45699-6_8"},{"key":"S0956796807006624_manual_ref-26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54152-7_66"},{"key":"S0956796807006624_manual_ref-11","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00348-0"},{"key":"S0956796807006624_manual_ref-21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90009-8"},{"key":"S0956796807006624_manual_ref-46","unstructured":"Schmidt-Schau\u00df, M. , Sch\u00fctz, M. , & Sabel, D. (2004) On the safety of N\u00f6cker's strictness analysis. Tech. Rept. Frank-19. Institut f\u00fcr Informatik. J.W. Goethe-University."},{"key":"S0956796807006624_manual_ref-3","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2651"},{"key":"S0956796807006624_manual_ref-1","volume-title":"Abstract Interpretation of Declarative Languages","author":"Abramsky","year":"1987"},{"key":"S0956796807006624_manual_ref-12","volume-title":"Conference Record of the Fourth ACM Symposium on Principles of Programming Languages.","author":"Cousot","year":"1977"},{"key":"S0956796807006624_manual_ref-25","unstructured":"Mycroft, Alan. (1981) Abstract interpretation and optimising transformations for applicative programs. Ph.D. thesis, University of Edinburgh."},{"key":"S0956796807006624_manual_ref-36","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90014-0"},{"key":"S0956796807006624_manual_ref-18","first-page":"257","volume-title":"Proc. RTA 95.","author":"Kennaway","year":"1993"},{"key":"S0956796807006624_manual_ref-9","volume-title":"Lazy Functional Languages: Abstract Interpretation and Compilation.","author":"Burn","year":"1991"},{"key":"S0956796807006624_manual_ref-17","first-page":"209","volume-title":"Symposium on Principles of Programming Languages.","author":"Jensen","year":"1998"},{"key":"S0956796807006624_manual_ref-35","first-page":"184","volume-title":"Functional programming, Glasgow 1994.","author":"Peyton","year":"1994"},{"key":"S0956796807006624_manual_ref-40","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"#cr-split#-S0956796807006624_manual_ref-47.1","unstructured":"Schmidt-Schau\u00df, M. , Sch\u00fctz, M. & Sabel, D. (2005) Deciding subset relationship of co-inductively defined set constants. Tech. Rept. Frank-23. Institut f\u00fcr Informatik. J.W. Goethe-University. report revised in 2006"},{"key":"#cr-split#-S0956796807006624_manual_ref-47.2","unstructured":"published as Schmidt-Schau\u00df et al. (2007) in 2007."},{"key":"S0956796807006624_manual_ref-29","first-page":"255","volume-title":"Functional Programming Languages and Computer Architecture","author":"N\u00f6cker","year":"1993"},{"key":"S0956796807006624_manual_ref-2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00104-X"},{"key":"S0956796807006624_manual_ref-37","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"S0956796807006624_manual_ref-41","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36377-7_4"},{"key":"S0956796807006624_manual_ref-45","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60360-3_49"},{"key":"S0956796807006624_manual_ref-22","unstructured":"Mann, Matthias. (2004) Towards sharing in lazy computation systems. Frank Report 18. Institut f\u00fcr Informatik, J. W. Goethe-Universit\u00e4t Frankfurt, Germany."},{"key":"S0956796807006624_manual_ref-34","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004331"},{"key":"S0956796807006624_manual_ref-50","unstructured":"Sch\u00fctz, M. (2000) Analysing Demand in Nonstrict Functional Programming Languages. Dissertation, J.W. Goethe-Universit\u00e4t Frankfurt. Available at http:\/\/www.ki.informatik.uni-frankfurt.de\/papers\/marko."},{"key":"S0956796807006624_manual_ref-10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45099-3_6"},{"key":"S0956796807006624_manual_ref-53","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18317-5_21"},{"key":"S0956796807006624_manual_ref-39","unstructured":"Plasmeijer, R. , & vanEekelen, M. Eekelen, M. (2003) The Concurrent Clean Language Report: Version 1.3 and 2.0. Tech. rept. Dept. of Computer Science, University of Nijmegen. http:\/\/www.cs.kun.nl\/~clean\/."},{"key":"S0956796807006624_manual_ref-28","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165219"},{"key":"S0956796807006624_manual_ref-23","first-page":"43","volume-title":"POPL 1999.","author":"Moran","year":"1999"},{"key":"S0956796807006624_manual_ref-24","first-page":"85","volume-title":"Coordination '99. Lecture Notes in Computer Science","author":"Moran","year":"1999"},{"key":"S0956796807006624_manual_ref-13","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2773"},{"key":"S0956796807006624_manual_ref-27","unstructured":"N\u00f6cker, Eric. (1990) Strictness analysis using abstract reduction. Technical Report 90-14. Department of Computer Science, University of Nijmegen."},{"key":"S0956796807006624_manual_ref-43","unstructured":"Schmidt-Schau\u00df, M. (2003) FUNDIO: A lambda-calculus with a letrec, case, constructors, and an IO-interface: Approaching a theory of unsafePerformIO. Frank report 16. Institut f\u00fcr Informatik, J.W. Goethe-Universit\u00e4t Frankfurt am Main."},{"key":"S0956796807006624_manual_ref-44","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006624"},{"key":"S0956796807006624_manual_ref-6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:10Z","timestamp":1776889150000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006624\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11,8]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["S0956796807006624"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006624","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,11,8]]}}}