{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:19:53Z","timestamp":1725761993696},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642452208"},{"type":"electronic","value":"9783642452215"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_19","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"258-273","source":"Crossref","is-referenced-by-count":0,"title":["Complexity Analysis in Presence of Control Operators and Higher-Order Functions"],"prefix":"10.1007","author":[{"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[]},{"given":"Giulio","family":"Pellitta","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Accattoli, B., Dal Lago, U.: On the invariance of the unitary cost model for head reduction. In: RTA. LIPIcs, vol.\u00a015, pp. 22\u201337 (2012)","key":"19_CR1"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1007\/3-540-45061-0_68","volume-title":"Automata, Languages and Programming","author":"Z.M. Ariola","year":"2003","unstructured":"Ariola, Z.M., Herbelin, H.: Minimal classical logic and control operators. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 871\u2013885. Springer, Heidelberg (2003)"},{"issue":"2","key":"19_CR3","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/j.ic.2010.10.002","volume":"209","author":"P. Baillot","year":"2011","unstructured":"Baillot, P., Coppola, P., Dal Lago, U.: Light logics and optimal reduction: Completeness and complexity. Information and Computation\u00a0209(2), 118\u2013142 (2011)","journal-title":"Information and Computation"},{"issue":"2","key":"19_CR4","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.tcs.2009.09.015","volume":"411","author":"P. Baillot","year":"2010","unstructured":"Baillot, P., Mazza, D.: Linear logic by levels and bounded time complexity. Theoretical Computer Science\u00a0411(2), 470\u2013503 (2010)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.ic.2008.08.005","volume":"207","author":"P. Baillot","year":"2009","unstructured":"Baillot, P., Terui, K.: Light types for polynomial time computation in lambda-calculus. Information and Computation\u00a0207(1), 41\u201362 (2009)","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP, pp. 233\u2013243. ACM (2000)","key":"19_CR6","DOI":"10.1145\/357766.351262"},{"doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. Logical Methods in Computer Science\u00a08(4) (2012)","key":"19_CR7","DOI":"10.2168\/LMCS-8(4:11)2012"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-02273-9_8","volume-title":"Typed Lambda Calculi and Applications","author":"U. Lago Dal","year":"2009","unstructured":"Dal Lago, U., Hofmann, M.: Bounded linear logic, revisited. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 80\u201394. Springer, Heidelberg (2009)"},{"unstructured":"Dal Lago, U., Pellitta, G.: Complexity analysis in presence of control operators and higher-order functions (long version), \n                  \n                    http:\/\/arxiv.org\/abs\/1310.1763","key":"19_CR9"},{"unstructured":"de Bakker, J.W., de Bruin, A., Zucker, J.: Mathematical theory of program correctness. Prentice-Hall International Series in Computer Science. Prentice Hall (1980)","key":"19_CR10"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0017475","volume-title":"Trees in Algebra and Programming - CAAP \u201994","author":"P. Groote de","year":"1994","unstructured":"de Groote, P.: A CPS-translation of the \u03bb\u03bc-calculus. In: Tison, S. (ed.) CAAP 1994. LNCS, vol.\u00a0787, pp. 85\u201399. Springer, Heidelberg (1994)"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-58216-9_27","volume-title":"Logic Programming and Automated Reasoning","author":"P. Groote de","year":"1994","unstructured":"de Groote, P.: On the relation between the \u03bb\u03bc-calculus and the syntactic theory of sequential control. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol.\u00a0822, pp. 31\u201343. Springer, Heidelberg (1994)"},{"issue":"6","key":"19_CR13","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1017\/S0960129598002667","volume":"8","author":"P. Groote de","year":"1998","unstructured":"de Groote, P.: An environment machine for the \u03bb\u03bc-calculus. Mathematical Structures in Computer Science\u00a08(6), 637\u2013669 (1998)","journal-title":"Mathematical Structures in Computer Science"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-52592-0_60","volume-title":"ESOP 1990","author":"M. Felleisen","year":"1990","unstructured":"Felleisen, M.: On the expressive power of programming languages. In: Jones, N. (ed.) ESOP 1990. LNCS, vol.\u00a0432, pp. 134\u2013151. Springer, Heidelberg (1990)"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-74915-8_21","volume-title":"Computer Science Logic","author":"M. Gaboardi","year":"2007","unstructured":"Gaboardi, M., Ronchi Della Rocca, S.: A soft type assignment system for lambda-calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 253\u2013267. Springer, Heidelberg (2007)"},{"issue":"1","key":"19_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050(1), 1\u2013101 (1987)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"19_CR17","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"Girard, J.-Y.: A new constructive logic: Classical logic. Mathematical Structures in Computer Science\u00a01(3), 255\u2013296 (1991)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"2","key":"19_CR18","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1006\/inco.1998.2700","volume":"143","author":"J.-Y. Girard","year":"1998","unstructured":"Girard, J.-Y.: Light linear logic. Information and Computation\u00a0143(2), 175\u2013204 (1998)","journal-title":"Information and Computation"},{"issue":"1","key":"19_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(92)90386-T","volume":"97","author":"J.-Y. Girard","year":"1992","unstructured":"Girard, J.-Y., Scedrov, A., Scott, P.: Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science\u00a097(1), 1\u201366 (1992)","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Griffin, T.: A formulae-as-types notion of control. In: POPL, pp. 47\u201358. ACM Press (1990)","key":"19_CR20","DOI":"10.1145\/96709.96714"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-02658-4_7","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S.: Speed: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 51\u201362. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Jost, S., Hammond, K., Loidl, H.-W., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: POPL, Madrid, Spain. ACM Press (2010)","key":"19_CR22","DOI":"10.1145\/1706299.1706327"},{"issue":"1","key":"19_CR23","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.tcs.2003.10.018","volume":"318","author":"Y. Lafont","year":"2004","unstructured":"Lafont, Y.: Soft linear logic and polynomial time. Theoretical Computer Science\u00a0318(1), 163\u2013180 (2004)","journal-title":"Theoretical Computer Science"},{"unstructured":"Laurent, O.: \u00c9tude de la polarisation en logique. Th\u00e8se de doctorat, Universit\u00e9 Aix-Marseille\u00a0II (March 2002)","key":"19_CR24"},{"issue":"1","key":"19_CR25","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/S0304-3975(01)00297-3","volume":"290","author":"O. Laurent","year":"2003","unstructured":"Laurent, O.: Polarized proof-nets and \u03bb\u03bc-calculus. Theoretical Computer Science\u00a0290(1), 161\u2013188 (2003)","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: POPL, pp. 215\u2013227. ACM Press (1997)","key":"19_CR26","DOI":"10.1145\/263699.263722"},{"key":"19_CR27","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb\u03bc-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS (LNAI), vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"doi-asserted-by":"crossref","unstructured":"Sch\u00f6pp, U.: Stratified bounded affine logic for logarithmic space. In: LICS, pp. 411\u2013420 (2007)","key":"19_CR28","DOI":"10.1109\/LICS.2007.45"},{"doi-asserted-by":"crossref","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenstr\u00f6m, P.: The worst case execution time problem - overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems (2008)","key":"19_CR29","DOI":"10.1145\/1347375.1347389"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45221-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T04:41:33Z","timestamp":1558759293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}