{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T18:34:45Z","timestamp":1649097285737},"reference-count":15,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4064,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,6]]},"DOI":"10.1016\/s0304-3975(01)00138-4","type":"journal-article","created":{"date-parts":[[2002,10,11]],"date-time":"2002-10-11T11:37:18Z","timestamp":1034336238000},"page":"305-331","source":"Crossref","is-referenced-by-count":1,"title":["Correctness of Java card method lookup via logical relations"],"prefix":"10.1016","volume":"283","author":[{"given":"Ewen","family":"Denney","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(01)00138-4_BIB1","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin, A. Sa\u0131\u0308bi, B. Werner, The Coq Proof Assistant Reference Manual\u2014Version V6.1, Tech. Report 0203, INRIA, August 1997."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB2","unstructured":"P. Bertelsen, Semantics of Java byte code, Tech. Report, Department of Information Technology, Technical University of Denmark, March 1997."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB3","series-title":"Proc. 23rd Internat. Symp. on Mathematical Foundations of Computer Science, Lecture Notes in Computer Sciences, vol. 1450","article-title":"Defining the Java virtual machine as platform for provably correct Java compilation","author":"B\u00f6rger","year":"1998"},{"key":"10.1016\/S0304-3975(01)00138-4_BIB4","unstructured":"E. Denney, Correctness of Java Card Tokenisation, Tech. Report 1286, Project Lande, IRISA, 1999. Also appears as INRIA research report 3831."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB5","unstructured":"J.-L. Lanet, A. Requet, Formal proof of smart card applets correctness, Third Smart Card Research and Advanced Conf. (CARDIS\u201998), 1998."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB6","series-title":"The Java Virtual Machine Specification","author":"Lindholm","year":"1997"},{"key":"10.1016\/S0304-3975(01)00138-4_BIB7","series-title":"Foundations for Programming Languages, Foundations of Computing Series","author":"Mitchell","year":"1996"},{"key":"10.1016\/S0304-3975(01)00138-4_BIB8","unstructured":"D. Mosses, Modularity in structural operational sematics, Extended abstract, November 1998."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB9","series-title":"Theorem Proving in Higher Order Logics (TPHOLs\u201996)","first-page":"347","article-title":"Verification of Compiler Correctness for the WAM","author":"Pusch","year":"1996"},{"key":"10.1016\/S0304-3975(01)00138-4_BIB10","unstructured":"C. Pusch, Formalizing the Java Virtual Machine in Isabelle\/HOL, Tech. Report TUM-I9816, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 1998."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB11","series-title":"Types, abstraction and parametric polymorphism, Information Processing 83","author":"Reynolds","year":"1983"},{"key":"10.1016\/S0304-3975(01)00138-4_BIB12","unstructured":"G. Schellhorn, Verification of abstract state machines, Ph.D. Thesis, University of Ulm, 1999."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB13","unstructured":"G. Segouat, Preuve en Coq d'une mise en oeuvre de Java Card, Master's Thesis, Project Lande, IRISA, 1999."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB14","unstructured":"Sun Microsystems, Java Card 2.0 Language Subset and Virtual Machine Specification, October 1997, Final Revision."},{"key":"10.1016\/S0304-3975(01)00138-4_BIB15","unstructured":"Sun Microsystems, Java Card 2.1 Virtual Machine Specification, March 1999, Final Revision 1.0."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001384?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001384?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,11]],"date-time":"2019-04-11T09:25:23Z","timestamp":1554974723000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397501001384"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["S0304397501001384"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(01)00138-4","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,6]]}}}