{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:07:55Z","timestamp":1751983675018},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617396"},{"type":"electronic","value":"9783540706748"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61739-6_39","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:18:33Z","timestamp":1330276713000},"page":"143-158","source":"Crossref","is-referenced-by-count":6,"title":["Refinement types for program analysis"],"prefix":"10.1007","author":[{"given":"Mario","family":"Coppo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ferruccio","family":"Damiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paola","family":"Giannini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"11_CR1","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:931\u2013940, 1983.","journal-title":"Journal of Symbolic Logic"},{"key":"11_CR2","unstructured":"S. Berardi. Pruning Simply Typed Lambda Terms. Journal of Symbolic Computation, to appear."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"S. Berardi and L. Boerio. Using Subtyping in Program Optimization. In Typed Lambda Calculus and Applications, 1995.","DOI":"10.1007\/BFb0014045"},{"issue":"4","key":"11_CR4","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"M. Coppo and M. Dezani-Ciancaglini. An extension of basic functional theory for lambda-calculus. Notre Dame Journal of Formal Logic, 21(4):685\u2013693, 1980.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"M. Coppo and A. Ferrari. Type inference, abstract interpretation and strictness analysis. In M. Dezani-Ciancaglini et al., editors, A collection of contributions in honour of Corrado B\u00f6hm, pages 113\u2013145. Elsevier, 1993.","DOI":"10.1016\/0304-3975(93)90086-9"},{"issue":"1","key":"11_CR6","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1006\/inco.1995.1141","volume":"122","author":"M. Coppo","year":"1995","unstructured":"M. Coppo and P. Giannini. Pricipal Types and Unification for Simple Intersection Types Systems. Information and Computation, 122(1):70\u201396, 1995.","journal-title":"Information and Computation"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"F. Damiani and P. Giannini. A Decidable Intersection Type System based on Relevance. In Theoretical Aspects of Computer Software, LNCS 789. Springer, 1994.","DOI":"10.1007\/3-540-57887-0_122"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"C. Hankin and D. Le Metayer. A Type-Based Framework for Program Analysis. In Static Analisys, LNCS 864, pages 380\u2013394. Springer, 1994.","DOI":"10.1007\/3-540-58485-4_53"},{"key":"11_CR9","first-page":"29","volume":"146","author":"R. Hindley","year":"1969","unstructured":"R. Hindley. The principal types schemes for an object in combinatory logic. Transactions of American Mathematical Society, 146:29\u201360, 1969.","journal-title":"Transactions of American Mathematical Society"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"L.S. Hunt and D. Sands. Binding Time Analysis: A New PERspective. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-based Program Manipulation, 1991.","DOI":"10.1145\/115865.115881"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"P. O'Keefe J. Palsberg. A Type System Equivalent to Flow Analysis. In Principles of Programming Languages, 1995.","DOI":"10.1145\/199448.199533"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"T. P. Jensen. Strictness Analysis in Logical Form. In J. Hughes, editor, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, pages 98\u2013105, 1991.","DOI":"10.1007\/3540543961_17"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"H. R. Nielson K. L. Solberg and F. Nielson. Strictness and Totality Analysis. In Static Analisys, LNCS 864, pages 408\u2013422. Springer, 1994.","DOI":"10.1007\/3-540-58485-4_55"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"D. Leivant. Polymorphic Type Inference. In Principles of Programming Languages, ACM, 1983.","DOI":"10.1145\/567067.567077"},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Science, 17:348\u2013375, 1978.","journal-title":"Journal of Computer and System Science"},{"key":"11_CR16","volume-title":"Technical report","author":"F. Prost","year":"1995","unstructured":"F. Prost. Marking techniques for extraction. Technical report, Ecole Normale Sup\u00e9rieure de Lyon, Lyon, December 1995."},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"T.M.Kuo and P.Mishra. Strictness analysis: a new perspective based on type inference. In Functional Programming Languages and Computer Architecture. ACM, 1989.","DOI":"10.1145\/99370.99390"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"D. A. Wright. A New Technique for Strictness Analysis. In Proceedings of TAP-SOFT'91, LNCS 494, pages 260\u2013272. Springer, 1991.","DOI":"10.1007\/3540539816_70"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61739-6_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:10:06Z","timestamp":1605629406000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61739-6_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617396","9783540706748"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61739-6_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}