{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:50:40Z","timestamp":1725544240459},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540336891"},{"type":"electronic","value":"9783540336914"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11741060_2","type":"book-chapter","created":{"date-parts":[[2006,4,27]],"date-time":"2006-04-27T13:42:07Z","timestamp":1146145327000},"page":"16-36","source":"Crossref","is-referenced-by-count":7,"title":["Mobile Resource Guarantees and Policies"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[]},{"given":"Kenneth","family":"MacKenzie","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-30142-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Aspinall","year":"2004","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 34\u201349. Springer, Heidelberg (2004)"},{"key":"2_CR2","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resources. Technical Report EDI-INF-RR-0296, Informatics, University of Edinburgh (July 2005)"},{"key":"2_CR3","unstructured":"Aspinall, D., Beringer, L., Momigliano, A.: Optimisation validation. Technical report, Informatics, University of Edinburgh (December 2005)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30569-9_1","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D. Aspinall","year":"2005","unstructured":"Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 1\u201326. Springer, Heidelberg (2005)"},{"key":"2_CR5","volume-title":"The Real-time Specification for Java","author":"G. Bollella","year":"2000","unstructured":"Bollella, G., et al.: The Real-time Specification for Java. Addison-Wesley, Reading (2000)"},{"key":"2_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-32275-7_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Beringer","year":"2005","unstructured":"Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic certification of heap consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 347\u2013362. Springer, Heidelberg (2005)"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1145\/504282.504293","volume-title":"OOPSLA 2001: Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications","author":"W. Binder","year":"2001","unstructured":"Binder, W., Hulaas, J.G., Villaz\u00f3n, A.: Portable resource control in Java. In: OOPSLA 2001: Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, pp. 139\u2013155. ACM Press, New York (2001)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Beringer, L., MacKenzie, K., Stark, I.: Grail: a functional form for imperative mobile code. Electronic Notes in Theoretical Computer Science\u00a085(1) (June 2003)","DOI":"10.1016\/S1571-0661(05)80083-0"},{"key":"2_CR9","volume-title":"Proceedings of SEFM 2005","author":"G. Barthe","year":"2005","unstructured":"Barthe, G., Pavlova, M., Schneider, G.: Precise analysis of memory consumption using program logics. In: Aichernig, B., Beckert, B. (eds.) Proceedings of SEFM 2005. IEEE Press, Los Alamitos (2005)"},{"key":"2_CR10","unstructured":"Campbell, B.: Folding stack memory usage prediction into heap. In: Proceedings of Quantitative Aspects of Programming Languages Workshop, ETAPS 2005 (April 2005)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-31987-0_22","volume-title":"Programming Languages and Systems","author":"A. Chander","year":"2005","unstructured":"Chander, A., Espinosa, D., Islam, N.: Enforcing resource bounds via static verification of dynamic checks. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 311\u2013325. Springer, Heidelberg (2005)"},{"key":"2_CR12","unstructured":"Czajkowski, G., Hahn, S., Skinner, G., Soper, P., Bryce, C.: Sun Microsystems. Technical Report TR-2003-124: A resource management interface for the Java platform (May 2003)"},{"key":"2_CR13","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/286936.286944","volume-title":"OOPSLA 1998: Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications","author":"G. Czajkowski","year":"1998","unstructured":"Czajkowski, G., von Eicken, T.: JRes: a resource accounting interface for Java. In: OOPSLA 1998: Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pp. 21\u201335. ACM Press, New York (1998)"},{"key":"2_CR14","first-page":"184","volume-title":"Proc. 27th Symp. Principles of Prog. Lang. (POPL)","author":"K. Crary","year":"2000","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: Proc. 27th Symp. Principles of Prog. Lang. (POPL), pp. 184\u2013198. ACM, New York (2000)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Gilmore, S., Prowse, M.: Proof-carrying bytecode. In: Proceedings of First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2005), Edinburgh, Scotland (April 2005)","DOI":"10.1016\/j.entcs.2005.02.038"},{"key":"2_CR16","series-title":"ACM SIGPLAN Notices","first-page":"185","volume-title":"Proceedings of the 30th ACM Symposium on Principles of Programming Languages","author":"M. Hofmann","year":"2003","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for firstorder functional programs. In: Proceedings of the 30th ACM Symposium on Principles of Programming Languages. ACM SIGPLAN Notices, vol.\u00a038, pp. 185\u2013197. ACM Press, New York (2003)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L.: Recursion and dynamic data structures in bounded space: towards embedded ML programming. In: Proc. International Conference on Functional Programming (ACM), Paris (September 1999)","DOI":"10.1145\/317636.317785"},{"key":"2_CR18","unstructured":"J-S. J-SEAL2 website. See, www.jseal2.com"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L.: Recursion and dynamic data structures in bounded space: towards embedded ML programming. In: Proc. International Conference on Functional Programming (ACM), Paris (September 1999)","DOI":"10.1145\/317636.317785"},{"key":"2_CR20","first-page":"29","volume":"4","author":"K. MacKenzie","year":"2004","unstructured":"MacKenzie, K., Wolverson, N.: Camelot and grail: resourceaware functional programming on the JVM. Trends in Functional Programing\u00a04, 29\u201346 (2004); Intellect","journal-title":"Trends in Functional Programing"},{"key":"#cr-split#-2_CR21.1","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (October 1998);"},{"key":"#cr-split#-2_CR21.2","unstructured":"Available as Technical Report CMU-CS-98-154"},{"issue":"2","key":"2_CR22","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"J.-P. Talpin","year":"1994","unstructured":"Talpin, J.-P., Jouvelot, P.: The type and effect discipline. Inf. Comput.\u00a0111(2), 245\u2013296 (1994)","journal-title":"Inf. Comput."},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-27861-0_6","volume-title":"Implementation of Functional Languages","author":"P. Vasconcelos","year":"2004","unstructured":"Vasconcelos, P., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Trinder, P., Michaelson, G.J., Pe\u00f1a, R. (eds.) IFL 2003. LNCS, vol.\u00a03145, pp. 86\u2013101. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Construction and Analysis of Safe, Secure, and Interoperable Smart Devices"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11741060_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,26]],"date-time":"2021-07-26T04:41:44Z","timestamp":1627274504000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11741060_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540336891","9783540336914"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11741060_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}