{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T19:38:47Z","timestamp":1790451527075,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540572640","type":"print"},{"value":"9783540480273","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-57264-3_46","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T07:34:13Z","timestamp":1330241653000},"page":"254-266","source":"Crossref","is-referenced-by-count":3,"title":["Usage analysis with natural reduction types"],"prefix":"10.1007","author":[{"given":"David A.","family":"Wright","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clement A.","family":"Baker-Finch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"22_CR1","unstructured":"A. R. Anderson and N. D. Belnap, Jr. Entailment: The Logic of Relevance and Necessity. Princeton University Press, 1975."},{"key":"22_CR2","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(88)90037-0","volume":"57","author":"A. Avron","year":"1988","unstructured":"A. Avron. The semantics and proof theory of linear logic. Theoretical Computer Science, 57:161\u2013184, 1988.","journal-title":"Theoretical Computer Science"},{"key":"22_CR3","unstructured":"C. A. Baker-Finch. Relevant logic and strictness analysis. In Workshop on Static Analysis, LaBRI, Bordeaux, pages 221\u2013228. Bigre 81\u201382, 1992."},{"key":"22_CR4","unstructured":"H.P. Barendregt. The Lambda-Calculus: its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1984."},{"issue":"4","key":"22_CR5","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1983","unstructured":"H.P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic, 48(4):931\u2013940, December 1983.","journal-title":"Journal of Symbolic Logic"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"H.P. Barendregt, J.R. Kennaway, J.W. Klop, and M.R. Sleep. Needed Reduction and Spine Strategies for the lambda-calculus. Technical report, Centre for Mathematics and Computer Science, May 1986.","DOI":"10.1016\/0890-5401(87)90001-0"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"P.N. Benton. Strictness Logic and Polymorphic Invariance. In Logical Foundations of Computer Science, pages 33\u201344, 20\u201324 July 1992.","DOI":"10.1007\/BFb0023861"},{"key":"22_CR8","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0167-6423(86)90010-9","volume":"7","author":"G.L. Burn","year":"1986","unstructured":"G.L. Burn, C.L. Hankin, and S. Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249\u2013278, 1986.","journal-title":"Science of Computer Programming"},{"key":"22_CR9","unstructured":"A. Church. The weak theory of implication. In Menne, Wilhelmy, and Angsil, editors, Kontrolliertes Denken, Untersuchungen zum Logikkalk\u00fcl und der Logik der Einzelwissenschaften, pages 22\u201337. Kommissions-verlag Karl Alber, 1951."},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"M. Coppo. An Extended Polymorphic Type System for Applicative Languages. In Mathematical Foundations of Computer Science, number 88 in Lecture Notes in Computer Science. Springer-Verlag, September 1980.","DOI":"10.1007\/BFb0022505"},{"key":"22_CR11","unstructured":"M. Coppo. Type Inference, Abstract Interpretation and Strictness Analysis. Draft manuscript, 1992."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM Symposium on Principles of Programming Languages, pages 238\u2013252. ACM, 1977.","DOI":"10.1145\/512950.512973"},{"key":"22_CR13","unstructured":"H.B. Curry and R. Feys. Combinatory Logic, Volume 1. Studies in Logic and the Foundations of Mathematics. North-Holland, 1958."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"J. M. Dunn. Relevance logic and entailment. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Vol. III. D. Reidel, 1986.","DOI":"10.1007\/978-94-009-5203-4_3"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"B. Goldberg. Detecting Sharing of Partial Applications in Functional Programs. In Functional Programming Languages and Computer Architecture, volume 274 of Lecture Notes in Computer Science. Springer-Verlag, 1987.","DOI":"10.1007\/3-540-18317-5_22"},{"key":"22_CR16","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF00262047","volume":"6","author":"G. Helman","year":"1977","unstructured":"G. Helman. Completeness of the normal typed fragment of the \u03bb-system U. Journal of Philosophical Logic, 6:33\u201346, 1977.","journal-title":"Journal of Philosophical Logic"},{"key":"22_CR17","unstructured":"G. Helman. Restricted Lambda Abstraction and the Interpretation of Some Non-Classical Logics. PhD thesis, University of Pittsburgh, 1977."},{"key":"22_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(83)90136-6","volume":"22","author":"J.R. Hindley","year":"1983","unstructured":"J.R. Hindley. The Completeness Theorem for Typing \u03bb-terms. Theoretical Computer Science, 22:1\u201317, 1983.","journal-title":"Theoretical Computer Science"},{"key":"22_CR19","unstructured":"W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatorial Logic, Lambda Calculus and Formalism, pages 479\u2013490. Academic Press, 1980."},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"P. Hudak and R. Young. Higher-order strictness analysis in untyped lambda calculus. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 97\u2013109. ACM, 1986.","DOI":"10.1145\/512644.512653"},{"key":"22_CR21","unstructured":"Bart Jacobs. Semantics of weakening and contraction. Technical report, Department of Pure Mathematics, University of Cambridge, 1992."},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"T.P. Jensen. Strictness Analysis in Logical Form, 1991.","DOI":"10.1007\/3540543961_17"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"T.P. Jensen and T.A. Mogensen. A Backwards Analysis for Compile-time Garbage Collection. In N.D. Jones, editor, European Symposium on Programming, volume 432 of Lecture Notes in Computer Science. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52592-0_66"},{"key":"22_CR24","unstructured":"J.W. Klop. Combinatory Reduction Systems. PhD thesis, State University of Utrecht, 1980."},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"T-M. Kuo and P. Mishra. Strictness Analysis: A New Perspective based on Type Inference. In FPCA '89, pages 260\u2013272, London, United Kingdom, September 1989.","DOI":"10.1145\/99370.99390"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"A. Mycroft. The theory and practice of transforming call-by-need into call-by-value. In International Symposium on Programming, volume 83 of Lecture Notes in Computer Science, pages 269\u2013281. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-09981-6_19"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"A. Mycroft and N. Jones. A relational framework for abstract interpretation. In Workshop on Programs as Data Objects, volume 217 of Lecture Notes in Computer Science, pages 156\u2013171. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-16446-4_9"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"G.D. Plotkin. A Semantics for Type Checking. In Theoretical Aspects of Computer Science, volume 526 of Lecture Notes in Computer Science, pages 1\u201317. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54415-1_38"},{"key":"22_CR29","unstructured":"P. Sestoft. Analysis and Efficient Implementation of Functional Programs. PhD thesis, DIKU, University of Copenhagen, 1991."},{"key":"22_CR30","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J.H. Siekmann","year":"1989","unstructured":"J.H. Siekmann. Unification Theory. Journal of Symbolic Computation, 7:207\u2013274, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"P. Wadler. Is there a use for Linear Logic? In Partial Evaluation and Program Manipulation. ACM Press, 1991.","DOI":"10.1145\/115865.115894"},{"key":"22_CR32","unstructured":"D.A. Wright. Strictness Analysis Via (Type) Inference. Technical Report TR89-3, University of Tasmania, September 1989."},{"key":"22_CR33","doi-asserted-by":"crossref","unstructured":"D.A. Wright. A New Technique for Strictness Analysis. In Theory and Practice of Software Development, number 494 in Lecture Notes in Computer Science. Springer-Verlag, April 1991.","DOI":"10.1007\/3540539816_70"},{"key":"22_CR34","unstructured":"D.A. Wright. Reduction Types and Intensionality in the Lambda-Calculus. PhD thesis, University of Tasmania, 1992."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57264-3_46.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T00:24:05Z","timestamp":1640910245000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57264-3_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540572640","9783540480273"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-57264-3_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}