{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T06:35:02Z","timestamp":1676961302400},"reference-count":35,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"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":3619,"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":[[2003,9]]},"DOI":"10.1016\/s1571-0661(05)80083-0","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T08:37:08Z","timestamp":1117010228000},"page":"3-23","source":"Crossref","is-referenced-by-count":7,"title":["Grail: a functional form for imperative mobile code"],"prefix":"10.1016","volume":"85","author":[{"given":"Lennart","family":"Beringer","sequence":"first","affiliation":[]},{"given":"Kenneth","family":"MacKenzie","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Stark","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80083-0_BIB1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b11938","article-title":"Max-plus quasi-interpretations, in: Typed Lambda Calculi and Applications: Proceedings of TLCA 2003","author":"Amadio","year":"2003"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB2","series-title":"\u201cCompiling with Continuations,\u201d","author":"Appel","year":"1992"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB3","series-title":"ACM SIGPLAN Notices 33","first-page":"17","article-title":"SSA is functional programming","author":"Appel","year":"1998"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB4","series-title":"Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science","first-page":"247","article-title":"Foundational proof-carrying code","author":"Appel","year":"2001"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB5","series-title":"Conference Record of POPL '00: 27th ACM Symposium on Principles of Programming Languages","first-page":"243","article-title":"A semantic model of types and machine instructions for proof-carrying code","author":"Appel","year":"2000"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB6","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-45927-8_4","article-title":"Another type system for in-place update, Programming Languages and Systems: Proceedings of the 11th European Symposium on Programming, ESOP 2002","volume":"2305","author":"Aspinall","year":"2002","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB7","series-title":"Technical Report ECS-LFCS-96-347, Laboratory for Foundations of Computer Science, University of Edinburgh","article-title":"Dual intuitionistic linear logic","author":"Barber","year":"1996"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB8","series-title":"\u201cAsynchronous Queue Machines with Explicit Forwarding,\u201d Ph.D. thesis, University of Edinburgh","author":"Beringer","year":"2002"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB9","series-title":"Laboratory for Foundations of Computer Science, University of Edinburgh","article-title":"Cost model","author":"Beringer","year":"2002"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB10","volume":"ECMA-335","author":"ECMA International","year":"2002"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB11","series-title":"SIGPLAN Notices, 28(6)","first-page":"237","article-title":"The essence of compiling with continuations, in: Proceedings of the 1993 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Flanagan","year":"1993"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB12","series-title":"20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation (1979-1999): A Selection","article-title":"Retrospective on \u201cThe essence of compiling with continuations\u201d","author":"Flanagan","year":"2003"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB13","first-page":"1","article-title":"Linear logic","volume":"46","author":"Girard","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB14","first-page":"258","article-title":"A type system for bounded space and functional in-place update","volume":"7","author":"Hofmann","year":"2000","journal-title":"Nordic Journal of Computing"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB15","series-title":"Conference Record of POPL '03: 30th ACM Symposium on Principles of Programming Languages","first-page":"185","article-title":"Static prediction of heap space usage for first-order functional programs","author":"Hofmann","year":"2003"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB16","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/3-540-39185-1_11","article-title":"Typing with conditions and guarantees in LFPL, in: Types for Proofs and Programs: Proceedings of the International Workshop TYPES 2002","volume":"2646","author":"Kone\u010dn\u00fd","year":"2002","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB17","series-title":"Workshop on Intermediate Representation Engineering for the Java Virtual Machine","article-title":"Functional Java bytecode, in: Proceedings of the 5th World Multi conference on Systemics, Cybernetics and Informatics","author":"League","year":"2001"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB18","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1002\/spe.438","article-title":"Bytecode verification for Java smart cards","volume":"32","author":"Leroy","year":"2002","journal-title":"Software Practice & Experience"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB19","series-title":"The Java Series","article-title":"\u201cThe Java Virtual Machine Specification,\u201d","author":"Lindholm","year":"1997"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB20","series-title":"Laboratory for Foundations of Computer Science, University of Edinburgh","article-title":"Grail: A functional intermediate language for resource bounded computation, version 1.2","author":"MacKenzie","year":"2002"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB21","series-title":"Laboratory for Foundations of Computer Science, University of Edinburgh","article-title":"JVML and .NET","author":"MacKenzie","year":"2002"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB22","series-title":"Laboratory for Foundations of Computer Science, University of Edinburgh","article-title":"From Camelot to Grail: Compiling a high-level language","author":"MacKenzie","year":"2003"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB23","unstructured":"Microsoft, Overview of the .NET framework, in: .NET Framework Developer's Guide, http:\/\/msdn.microsoft.com."},{"key":"10.1016\/S1571-0661(05)80083-0_BIB24","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1145\/319301.319345","article-title":"From System F to typed assembly language","volume":"21","author":"Morrisett","year":"1999","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB25","unstructured":"MRG, Mobile resource guarantees (2002-2004), www.lfcs.ed.ac.uk\/mrg."},{"key":"10.1016\/S1571-0661(05)80083-0_BIB26","series-title":"Conference Record of POPL '97: 24th ACM Symposium on Principles of Programming Languages","first-page":"106","article-title":"Proof-carrying code","author":"Necula","year":"1997"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB27","series-title":"\u201cPrinciples of Program Analysis,\u201d Springer","author":"Nielson","year":"1999"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB28","volume":"2283","author":"Nipkow","year":"2002"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB29","first-page":"89","article-title":"Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited, in: Formal Methods Europe 2002","volume":"2391","author":"Oheimb","year":"2002","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB30","series-title":"Separation logic: A logic for shared mutable data structures, in: Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science","first-page":"55","author":"Reynolds","year":"2002"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB31","series-title":"\u201cStrange Case of Dr. Jekyll and Mr. Hyde,\u201d Longmans, Green, London","author":"Stevenson","year":"1886"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB32","series-title":"\u201cJava Card 2.2 Platform Specification,\u201d","author":"Sun Microsystems","year":"2003"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB33","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/S0304-3975(99)00054-7","article-title":"Operational interpretations of linear logic","volume":"227","author":"Turner","year":"1999","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB34","series-title":"number 598 in Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/3-540-55511-0_15","article-title":"Correctness of procedure representations in higher-order assembly language, in: Mathematical Foundations of Programming Semantics '91: Proceedings of the 7th International Conference","author":"Wand","year":"1992"},{"key":"10.1016\/S1571-0661(05)80083-0_BIB35","series-title":"Laboratory for Foundations of Computer Science, University of Edinburgh","article-title":"Optimisation and resource bounds in Camelot compilation","author":"Wolverson","year":"2003"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800830?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800830?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T03:58:37Z","timestamp":1548475117000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105800830"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105800830"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80083-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}