{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:09:51Z","timestamp":1725491391429},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540744634"},{"type":"electronic","value":"9783540744641"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74464-1_15","type":"book-chapter","created":{"date-parts":[[2007,9,12]],"date-time":"2007-09-12T02:58:12Z","timestamp":1189565892000},"page":"221-236","source":"Crossref","is-referenced-by-count":1,"title":["Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs"],"prefix":"10.1007","author":[{"given":"Hugo R.","family":"Sim\u00f5es","sequence":"first","affiliation":[]},{"given":"Kevin","family":"Hammond","sequence":"additional","affiliation":[]},{"given":"M\u00e1rio","family":"Florido","sequence":"additional","affiliation":[]},{"given":"Pedro","family":"Vasconcelos","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Nielson, F., Nielson, H.R.: Type and Effect Systems: Behaviours for Concurrency. Imperial College Press (1999)","DOI":"10.1142\/p132"},{"issue":"1","key":"15_CR2","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1017\/S0960129502003845","volume":"13","author":"A. Banerjee","year":"2003","unstructured":"Banerjee, A., Jensen, T.: Modular control-flow analysis with rank 2 intersection types. Mathematical. Structures in Comp. Sci.\u00a013(1), 87\u2013124 (2003)","journal-title":"Mathematical. Structures in Comp. Sci."},{"key":"15_CR3","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus. Its Syntax and Semantics. In: Studies in Logic and the Foundations of Mathematics, vol.\u00a0103, North-Holland, Amsterdam (1984)"},{"issue":"4","key":"15_CR4","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H. Barendregt","year":"1983","unstructured":"Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic\u00a048(4), 931\u2013940 (1983)","journal-title":"The Journal of Symbolic Logic"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/978-3-540-24725-8_21","volume-title":"Programming Languages and Systems","author":"S. Carlier","year":"2004","unstructured":"Carlier, S., Polakow, J., Wells, J.B., Kfoury, A.J.: System e: Expansion variables for flexible typing with linear and non-linear types and intersection types. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 294\u2013309. Springer, Heidelberg (2004)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Chin, W.-N., Khoo, S.-C.: Calculating Sized Types. Higher-Order and Symbolic Computing 14(2,3) (2001)","DOI":"10.1023\/A:1012996816178"},{"issue":"4","key":"15_CR7","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the \u03bb-calculus. Notre-Dame Journal of Formal Logic\u00a021(4), 685\u2013693 (1980)","journal-title":"Notre-Dame Journal of Formal Logic"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Coppo, M., Giannini, P.: Principal types and unification for simple intersection type systems. Information and Computation 122(1) (1995)","DOI":"10.1006\/inco.1995.1141"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/11780342_11","volume-title":"Logical Approaches to Computational Barriers","author":"U.D. Lago","year":"2006","unstructured":"Lago, U.D., Martini, S.: An invariant cost model for the lambda calculus. In: Beckmann, A., Berger, U., L\u00f6we, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol.\u00a03988, pp. 105\u2013114. Springer, Heidelberg (2006)"},{"issue":"4","key":"15_CR10","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1145\/778559.778560","volume":"25","author":"F. Damiani","year":"2003","unstructured":"Damiani, F.: Rank 2 intersection types for local definitions and conditional expressions. ACM Transactions On Programming Languages and Systems\u00a025(4), 401\u2013451 (2003)","journal-title":"ACM Transactions On Programming Languages and Systems"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Theoretical Aspects of Computer Science","author":"F. Damiani","year":"1994","unstructured":"Damiani, F., Giannini, P.: A decidable intersection type system based on relevance. In: Theoretical Aspects of Computer Science. LNCS, Springer, Heidelberg (1994)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/11417170_12","volume-title":"Typed Lambda Calculi and Applications","author":"F. Damiani","year":"2005","unstructured":"Damiani, F.: Rank-2 Intersection and Polymorphic Recursion. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 146\u2013161. Springer, Heidelberg (2005)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Davies, R., Pfenning, F.: Intersection types and computational effects. In: ICFP, pp. 198\u2013208 (2000)","DOI":"10.1145\/351240.351259"},{"issue":"1","key":"15_CR14","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/130616.130620","volume":"1","author":"V. Dornic","year":"1992","unstructured":"Dornic, V., Jouvelot, P., Gifford, D.K.: Polymorphic Time Systems for Estimating Program Complexity. ACM Letters on Prog. Lang. and Systems\u00a01(1), 33\u201345 (1992)","journal-title":"ACM Letters on Prog. Lang. and Systems"},{"key":"15_CR15","first-page":"193","volume-title":"Formal Description of Programming Concepts III","author":"M. Felleisen","year":"1986","unstructured":"Felleisen, M., Friedman, D.P.: Control Operators, the SECD-Machine and the \u03bb-Calculus. In: Wirsing, M. (ed.) Formal Description of Programming Concepts III, pp. 193\u2013217. Elsevier, Amsterdam (1986)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Grobauer, B.: Cost Recurrences for DML Programs. In: Proc. 2001 ACM Intl. Conf. on Functional Programming \u2013 ICFP\u00a02001, Florence, Italy (September 2001)","DOI":"10.1145\/507635.507666"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/11693024_3","volume-title":"Programming Languages and Systems","author":"M. Hofmann","year":"2006","unstructured":"Hofmann, M., Jost, S.: Type-based amortised heap-space analysis (for an object-oriented language). In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 22\u201337. Springer, Heidelberg (2006)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Hughes, R.J.M., Pareto, L., Sabry, A.: Proving the Correctness of Reactive Systems using Sized Types. In: Proc. 1996 ACM Symposium on Principles of Programming Languages \u2013 POPL 1996, St Petersburg, FL (January 1996)","DOI":"10.1145\/237721.240882"},{"key":"15_CR19","unstructured":"Jim, T.: Rank 2 type systems and recursive definitions. Technical Report MIT\/LCS\/TM-531, Massachusetts Institute of Technology, Laboratory for Computer Science (November 1995)"},{"key":"15_CR20","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1145\/292540.292556","volume-title":"popl99","author":"A.J. Kfoury","year":"1999","unstructured":"Kfoury, A.J., Wells, J.B.: Principality and decidable type inference for finite-rank intersection types. In: Assaf, J. (ed.) popl99, pp. 161\u2013174. ACM Press, New York (1999)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Launchbury, J.: A Natural Semantics for Lazy Evaluation. In: Proc. 1993 ACM Symp. on Principles of Prog. Langs. \u2013 POPL 1993, pp. 144\u2013154 (1993)","DOI":"10.1145\/158511.158618"},{"issue":"3","key":"15_CR22","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"A.J.R.G. Milner","year":"1976","unstructured":"Milner, A.J.R.G.: A Theory of Type Polymorphism in Programming. J. Computer System Sciences\u00a017(3), 348\u2013375 (1976)","journal-title":"J. Computer System Sciences"},{"key":"15_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"key":"15_CR24","first-page":"561","volume-title":"To H.B. Curry, Essays in Combinatory Logic, Lambda-calculus and Formalism","author":"G. Pottinger","year":"1980","unstructured":"Pottinger, G.: A type assignement for the strongly normalizable terms. In: Hindley, J.R., Seldin, J.P. (eds.) To H.B. Curry, Essays in Combinatory Logic, Lambda-calculus and Formalism, pp. 561\u2013577. Academic Press, San Diego (1980)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-44854-3_15","volume-title":"Implementation of Functional Languages","author":"A.J.R. Portillo","year":"2003","unstructured":"Portillo, A.J.R., Hammond, K., Loidl, H.-W., Vasconcelos, P.: Cost analysis using automatic size and time inference. In: Pe\u00f1a, R., Arts, T. (eds.) IFL 2002. LNCS, vol.\u00a02670, pp. 232\u2013247. Springer, Heidelberg (2003)"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Reistad, B., Gifford, D.K.: Static Dependent Costs for Estimating Execution Time. In: Proc. 1994 ACM Conference on Lisp and Functional Programming \u2013 LFP 1994, pp. 65\u201378, Orlando, FL (June 1994)","DOI":"10.1145\/182409.182439"},{"key":"15_CR27","unstructured":"Simoes, H.R., Hammond, K., Florido, M., Vasconcelos, P.: Using intersection types for cost-analysis of higher-order polymorphic functional programs. Technical report (2006), http:\/\/www.dcs.st-and.ac.uk\/~kh\/papers\/itypes_cost.pdf"},{"key":"15_CR28","unstructured":"van Bakel, S.: Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Department of Computer Science, University of Nijmegen (1993)"},{"issue":"2","key":"15_CR29","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/FI-1996-26204","volume":"26","author":"S. Bakel van","year":"1996","unstructured":"van Bakel, S.: Rank 2 intersection type assignment in term rewriting systems. Fundam. Inform.\u00a026(2), 141\u2013166 (1996)","journal-title":"Fundam. Inform."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74464-1_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T23:51:09Z","timestamp":1684021869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74464-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540744634","9783540744641"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74464-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}