{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T16:41:12Z","timestamp":1740242472167,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242871"},{"type":"electronic","value":"9783540305699"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30569-9_1","type":"book-chapter","created":{"date-parts":[[2010,7,4]],"date-time":"2010-07-04T17:59:08Z","timestamp":1278266348000},"page":"1-26","source":"Crossref","is-referenced-by-count":23,"title":["Mobile Resource Guarantees for Smart Devices"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Gilmore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Donald","family":"Sannella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Stark","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","first-page":"247","volume-title":"Proceedings of LICS 2001","author":"A. Appel","year":"2001","unstructured":"Appel, A.: Foundational proof-carrying code. In: Proceedings of LICS 2001, pp. 247\u2013256. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"1_CR2","volume-title":"Compiling with Continuations","author":"A.W. Appel","year":"1992","unstructured":"Appel, A.W.: Compiling with Continuations. Cambridge University Press, Cambridge (1992)"},{"issue":"4","key":"1_CR3","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/278283.278285","volume":"33","author":"A.W. Appel","year":"1998","unstructured":"Appel, A.W.: SSA is functional programming. ACM SIGPLAN Notices\u00a033(4), 17\u201320 (1998)","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR4","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)"},{"issue":"3-4","key":"1_CR5","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/B:JARS.0000021014.79255.33","volume":"31","author":"D. Aspinall","year":"2003","unstructured":"Aspinall, D., Compagnoni, A.: Heap bounded assembly language. Journal of Automated Reasoning\u00a031(3-4), 261\u2013302 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-45927-8_4","volume-title":"Programming Languages and Systems","author":"D. Aspinall","year":"2002","unstructured":"Aspinall, D., Hofmann, M.: Another type system for in-place update. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 36\u201352. Springer, Heidelberg (2002)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Augustsson, L.: Cayenne - a language with dependent types. In: International Conference on Functional Programming, pp. 239\u2013250 (1998)","DOI":"10.1145\/291251.289451"},{"key":"1_CR8","unstructured":"Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Towards certificate generation for linear heap consumption. In: Proceedings of the ICALP\/LICS Workshop on Logics for Resources, Processes, and Programs, LRPP 2004 (2004)"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Beringer, L., MacKenzie, K., Stark, I.: Grail: a functional form for imperative mobile code. In: Foundations of Global Computing: Proceedings of the 2nd EATCS Workshop, number 85.1 in Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (June 2003)","DOI":"10.1016\/S1571-0661(05)80083-0"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P., Necula, G.C., Blau, F., Cline, K., Plesko, M.: A certifying compiler for Java. In: Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2000), Vancouver, Canada (2000)","DOI":"10.1145\/349299.349315"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: Proc. PDLI 1993, ACM SIGPLAN Notices, vol.\u00a028(6), pp. 237\u2013247 (1993)","DOI":"10.1145\/173262.155113"},{"key":"1_CR12","volume-title":"20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation (1979-1999): A Selection","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: Retrospective on \u201cThe essence of compiling with continuations\u201d. In: 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation (1979-1999): A Selection. ACM Press, New York (2003)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Foster, I., Kesselman, C., Lee, C., Lindell, R., Nahrstedt, K., Roy, A.: A distributed resource management architecture that supports advance reservations and co-allocation. In: Proceedings of the IEEE\/IFIP 7th International Workshop on Quality of Service (1999)","DOI":"10.1109\/IWQOS.1999.766475"},{"issue":"4","key":"1_CR14","first-page":"258","volume":"7","author":"M. Hofmann","year":"2000","unstructured":"Hofmann, M.: A type system for bounded space and functional in-place update. Nordic Journal of Computing\u00a07(4), 258\u2013289 (2000)","journal-title":"Nordic Journal of Computing"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0890-5401(03)00009-9","volume":"183","author":"M. Hofmann","year":"2003","unstructured":"Hofmann, M.: Linear types and non size-increasing polynomial time computation. Information and Computation\u00a0183, 57\u201385 (2003)","journal-title":"Information and Computation"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proceedings of the 30th ACM Symposium on Principles of Programming Languages, New Orleans (2003)","DOI":"10.1145\/604131.604148"},{"key":"1_CR17","unstructured":"Jost, S.: lfd_infer: an implementation of a static inference on heap space usage. In: Proceedings of Second Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, SPACE 2004 (2004)"},{"key":"1_CR18","unstructured":"Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, LFCS, University of Edinburgh (1999)"},{"key":"1_CR19","unstructured":"League, C., Trifonov, V., Shao, Z.: Functional Java bytecode. In: Proc. 5th SCI World Multiconference, Workshop on Intermediate Representation Engineering for the Java Virtual Machine. Internat. Inst. of Informatics and Systemics (July 2001)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Leavens, G., Leino, R., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, pp. 105\u2013106 (2000)","DOI":"10.1145\/367845.367996"},{"key":"1_CR21","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1002\/spe.438","volume":"32","author":"X. Leroy","year":"2002","unstructured":"Leroy, X.: Bytecode verification on Java smart cards. Software Practice & Experience\u00a032, 319\u2013340 (2002)","journal-title":"Software Practice & Experience"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. The Java Series. Addison-Wesley, Reading (January 1997)","DOI":"10.1007\/978-3-642-95851-9_5"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"MacKenzie, K., Wolverson, N.: Camelot and Grail: resource-aware functional programming for the JVM. In: Trends in Functional Programming, vol.\u00a04, pp. 29\u201346 (2004) (Intellect)","DOI":"10.2307\/j.ctv36xvxxx.6"},{"key":"1_CR24","unstructured":"Microsoft. Overview of the .NET framework. .NET Framework Developer\u2019s Guide, http:\/\/msdn.microsoft.com"},{"issue":"3","key":"1_CR25","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Transactions on Programming Languages and Systems\u00a021(3), 528\u2013569 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Proceedings of the ACM Symposium on Principles of Programming Languages (1997)","DOI":"10.1145\/263699.263712"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45793-3_8","volume-title":"Computer Science Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 103\u2013119. Springer, Heidelberg (2002)"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. In: Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.) Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"1_CR29","unstructured":"O\u2019Caml Web site. The O\u2019Caml Language, http:\/\/www.ocaml.org"},{"key":"1_CR30","unstructured":"Prowse, M.: Proving Grail resource bounds. University of Edinburgh (May 2003)"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: LICS 2002: Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Shaylor, N., Simon, D.N., Bush, W.R.: A Java virtual machine architecture for very small devices. In: Language, Compiler, and Tool Support for Embedded Systems: Proceedings of LCTES 2003, ACM SIGPLAN Notices, vol.\u00a038(7), pp. 31\u201341 (July 2003)","DOI":"10.1145\/780731.780738"},{"key":"1_CR33","unstructured":"Sun Microsystems. Java Card 2.2 Platform Specification (2003), available online at, http:\/\/java.sun.com\/products\/javacard\/specs.html"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/3-540-55511-0_15","volume-title":"Proc. MFPS 1991","author":"M. Wand","year":"1992","unstructured":"Wand, M.: Correctness of procedure representations in higher-order assembly language. In: Proc. MFPS 1991. LNCS, vol.\u00a0298, pp. 294\u2013311. Springer, Heidelberg (1992)"},{"key":"1_CR35","unstructured":"Wolverson, N.: Optimisation and resource bounds in Camelot compilation. Laboratory for Foundations of Computer Science, University of Edinburgh (2003)"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Wolverson, N., MacKenzie, K.: O\u2019Camelot: Adding objects to a resource aware functional language. In: Trends in Functional Programming, vol.\u00a04, pp. 47\u201362 (2004) (Intellect)","DOI":"10.2307\/j.ctv36xvxxx.7"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN Symposium on Principles of Programming Languages, San Antonio, pp. 214\u2013227 (January 1999)","DOI":"10.1145\/292540.292560"}],"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\/978-3-540-30569-9_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T16:14:25Z","timestamp":1740240865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30569-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242871","9783540305699"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30569-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}