{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:28:55Z","timestamp":1720625335570},"reference-count":15,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T00:00:00Z","timestamp":1346457600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":331,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2012,9]]},"DOI":"10.1016\/j.entcs.2012.08.010","type":"journal-article","created":{"date-parts":[[2012,9,27]],"date-time":"2012-09-27T20:15:39Z","timestamp":1348776939000},"page":"139-155","source":"Crossref","is-referenced-by-count":2,"special_numbering":"C","title":["Time Bounds for General Function Pointers"],"prefix":"10.1016","volume":"286","author":[{"given":"Robert","family":"Dockins","sequence":"first","affiliation":[]},{"given":"Aquinas","family":"Hobor","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2012.08.010_br0010","doi-asserted-by":"crossref","unstructured":"Ahmed, A., D. Dreyer and A. Rossberg, State-dependent representation independence, in: POPL \u02bc09: Proc. 36th annual Symposium on Principles of Programming Languages, 2009, pp. 340\u2013353.","DOI":"10.1145\/1594834.1480925"},{"key":"10.1016\/j.entcs.2012.08.010_br0020","unstructured":"Ahmed, A.J., \u201cSemantics of Types for Mutable State,\u201d Ph.D. thesis, Princeton University, Princeton, NJ (2004), tech Report TR-713-04."},{"key":"10.1016\/j.entcs.2012.08.010_br0030","author":"Appel"},{"key":"10.1016\/j.entcs.2012.08.010_br0040","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1016\/j.tcs.2007.09.003","article-title":"A program logic for resources","volume":"389","author":"Aspinall","year":"2007","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.entcs.2012.08.010_br0050","doi-asserted-by":"crossref","unstructured":"Barnett, M., B.-Y.E. Chang, R. DeLine, B. Jacobs and K.R.M. Leino, Boogie: A modular reusable verifier for object-oriented programs, in: 4th Intl. Symp. on Formal Methods for Components and Objects (FMCO05), 2005.","DOI":"10.1007\/11804192_17"},{"key":"10.1016\/j.entcs.2012.08.010_br0060","unstructured":"Birkedal, L., B. Reus, J. Schwinghammer, K. St\u00f8vring, J. Thamsborg and H. Yang, Step-indexed kripke models over recursive worlds, submitted for publication."},{"key":"10.1016\/j.entcs.2012.08.010_br0070","series-title":"Modelling, Controlling and Reasoning About State","article-title":"A theory of termination via indirection","volume":"vol. 10351","author":"Dockins","year":"2010"},{"key":"10.1016\/j.entcs.2012.08.010_br0080","unstructured":"Hobor, A., \u201cOracle Semanatics,\u201d Ph.D. thesis, Princeton University, Princeton, NJ (2008)."},{"key":"10.1016\/j.entcs.2012.08.010_br0090","unstructured":"A. Hobor, R. Dockins, and A. Appel. A logical mix of approximation and separation. In APLAS10."},{"key":"10.1016\/j.entcs.2012.08.010_br0100","doi-asserted-by":"crossref","unstructured":"Hobor, A., R. Dockins and A.W. Appel, A theory of indirection via approximation, in: Proc. 37th Annual ACM Symposium on Principles of Programming Languages (POPL\u02bc10), 2010, pp. 171\u2013185.","DOI":"10.1145\/1706299.1706322"},{"key":"10.1016\/j.entcs.2012.08.010_br0110","doi-asserted-by":"crossref","unstructured":"Honda, K., From process logic to program logic, in: ICFP \u02bc04: Proc. of the 9th intl. conference on Functional programming, 2004, pp. 163\u2013174.","DOI":"10.1145\/1016848.1016874"},{"key":"10.1016\/j.entcs.2012.08.010_br0120","series-title":"Automata, Languages and Programming","first-page":"360","article-title":"Descriptive and relative completeness of logics for higher-order functions","volume":"vol. 4052\/2006","author":"Honda","year":"2006"},{"key":"10.1016\/j.entcs.2012.08.010_br0130","doi-asserted-by":"crossref","unstructured":"Honda, K. and N. Yoshida, A compositional logic for polymorphic higher-order functions, in: PPDP \u02bc04: Proc. of the 6th intl. conference on Principles and practice of declarative programming, 2004, pp. 191\u2013202.","DOI":"10.1145\/1013963.1013985"},{"key":"10.1016\/j.entcs.2012.08.010_br0140","unstructured":"Richards, C.D., \u201cThe Approximation Modality in Models of Higher-Order Types,\u201d Ph.D. thesis, Princeton University, Princeton, NJ (2010)."},{"key":"10.1016\/j.entcs.2012.08.010_br0150","unstructured":"Schwinghammer, J., L. Birkedal, B. Reus and H. Yang, Nested hoare triples and frame rules for higher-order store, in: CSL\u02bc09\/EACSL\u02bc09: Proc. of the 23rd CSL intl. conference and 18th EACSL Annual conference on Computer science logic (2009), pp. 440\u2013454."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066112000400?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066112000400?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,7,4]],"date-time":"2019-07-04T04:02:57Z","timestamp":1562212977000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066112000400"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9]]},"references-count":15,"alternative-id":["S1571066112000400"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2012.08.010","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2012,9]]}}}