{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T19:52:44Z","timestamp":1648756364159},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,2,1]],"date-time":"2008-02-01T00:00:00Z","timestamp":1201824000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["New Gener. Comput."],"published-print":{"date-parts":[[2008,2]]},"DOI":"10.1007\/s00354-008-0038-8","type":"journal-article","created":{"date-parts":[[2008,4,30]],"date-time":"2008-04-30T14:11:43Z","timestamp":1209564703000},"page":"125-170","source":"Crossref","is-referenced-by-count":1,"title":["A New Type System for JVM Lock Primitives"],"prefix":"10.1007","volume":"26","author":[{"given":"Futoshi","family":"Iwama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,5,1]]},"reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"Barthe, G. and Rezk, T., \u201cNon-interference for a jvm-like language,\u201d in Proc. of ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2005), pp. 103\u2013112, 2005.","DOI":"10.1145\/1040294.1040304"},{"key":"38_CR2","unstructured":"Bigliardi, G. and Laneve, C., \u201cA type system for JVM threads,\u201d in Proc. of 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC2000), Montreal, Canada, 2000."},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"Chaki, S., Rajamani, S. and Rehof, J., \u201cTypes as models: Model checking message-passing programs,\u201d in Proc. of ACM SIGPLAN\/SIGACT Symp. on Principles of Programming Languages, pp. 45\u201357, 2002.","DOI":"10.1145\/503272.503278"},{"key":"38_CR4","unstructured":"Christensen, S., Decidability and Decomposition in Process Algebras. PhD. thesis, University of Edinburgh, 1993."},{"key":"38_CR5","doi-asserted-by":"crossref","unstructured":"DeLine, R. and F\u00e4hndrich, M., \u201cEnforcing high-level protocols in lowlevel software,\u201d in Proc. of ACM SIGPLAN Conf. on Programming Language Design and Implementation, pp. 59\u201369, 2001.","DOI":"10.1145\/381694.378811"},{"issue":"3","key":"38_CR6","first-page":"143","volume":"30","author":"J. Esparza","year":"1994","unstructured":"Esparza, J. and Nielsen, M., \u201cDecidability issues for Petri nets - a survey,\u201d Journal of Information Processing and Cybernetics, 30(3), pp. 143\u2013160, 1994.","journal-title":"Journal of Information Processing and Cybernetics"},{"key":"38_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C. and Abadi, M., \u201cObject types against races,\u201d in CONCUR\u2019 99, LNCS 1664, Springer-Verlag, pp. 288\u2013303, 1999.","DOI":"10.1007\/3-540-48320-9_21"},{"key":"38_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C. and Abadi, M., \u201cTypes for safe locking,\u201d in Proc. of ESOP 1999, LNCS 1576, pp. 91\u2013108, 1999.","DOI":"10.1007\/3-540-49099-X_7"},{"key":"38_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C. and Freund, S.N., \u201cType-based race detection for Java,\u201d in Proc. of ACM SIGPLAN Conf. on Programming Language Design and Implementation, pp. 219\u2013232, 2000.","DOI":"10.1145\/349299.349328"},{"key":"38_CR10","doi-asserted-by":"crossref","unstructured":"Foster, J.S., Terauchi, T. and Aiken, A., \u201cFlow-sensitive type qualifiers,\u201d in Proc. of ACM SIGPLAN Conf. on Programming Language Design and Implementation, 2002.","DOI":"10.1145\/512529.512531"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"Freund, S.N. and Mitchell. J.C., \u201cA type system for object initialization in the Java bytecode language,\u201d in OOPSLA \u201998: Proc. of the 13th ACM SIGPLAN conf. on Object-oriented programming, systems, languages, and applications, ACM Press, pp. 310\u2013327, New York, NY, USA, 1998.","DOI":"10.1145\/286936.286972"},{"issue":"3-4","key":"38_CR12","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1023\/A:1025011624925","volume":"30","author":"S.N. Freund","year":"2003","unstructured":"Freund, S.N. and Mitchell, J.C., \u201cA type system for the Java bytecode language and verifier,\u201d J. Autom. Reason, 30(3-4), pp. 271\u2013321, 2003.","journal-title":"J. Autom. Reason"},{"key":"38_CR13","unstructured":"Higuchi, T. and Ohori. A., \u201cJava bytecode as a typed term calculus. in ACM PPDP conf. 2002, ACM Press, pp. 201\u2013211, 2002."},{"issue":"1-3","key":"38_CR14","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0304-3975(03)00325-6","volume":"311","author":"A. Igarashi","year":"2004","unstructured":"Igarashi, A. and Kobayashi, N., \u201cA generic type system for the picalculus,\u201d Theoretical Computer Science, 311(1-3), pp. 121\u2013163, 2004.","journal-title":"Theoretical Computer Science"},{"key":"38_CR15","doi-asserted-by":"crossref","unstructured":"Igarashi, A. and Kobayashi, N., \u201cResource usage analysis,\u201d ACM Transactions on Programming Languages and Systems, 27(2), 2005. Preliminary summary appeared in Proc. of POPL 2002.","DOI":"10.1145\/1057387.1057390"},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Saito, S. and Sumii, E., \u201cAn implicitly-typed deadlockfree process calculus,\u201d in Proc. of CONCUR2000, LNCS 1877, Springer-Verlag, pp. 489-503, August 2000. The full version is available as technical report TR00-01, Dept. Info. Sci., Univ. Tokyo.","DOI":"10.1007\/3-540-44618-4_35"},{"key":"38_CR17","unstructured":"Kobayashi, N. and Shirane, K., \u201cType-based information flow analysis for low-level languages,\u201d Computer Software 20(2), pp. 2\u201321, 2003, in Japanese. A summary written in English appeared in informal proceedings of 2nd Asian Workshop on Programming Languages and Systems (APLAS\u201902)."},{"issue":"3:4","key":"38_CR18","first-page":"1","volume":"2","author":"N. Kobayashi","year":"2006","unstructured":"Kobayashi, N., Suenaga, K. and Wischik, L., \u201cResource usage analysis for the pi-calculus,\u201d Logical Methods in Computer Science, 2(3:4), pp. 1\u201342, 2006.","journal-title":"Logical Methods in Computer Science"},{"issue":"1","key":"38_CR19","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/S0304-3975(02)00330-4","volume":"290","author":"C. Laneve","year":"2003","unstructured":"Laneve, C., \u201cA type system for JVM Threads,\u201d Theoretical Computer Science, 290(1), pp. 241\u2013778, 2003.","journal-title":"Theoretical Computer Science"},{"key":"38_CR20","unstructured":"Lindholm, T. and Yellin, F., The Java Virtual Machine Specification (2 nd edition), Addison Wesley, 1999."},{"key":"38_CR21","doi-asserted-by":"crossref","unstructured":"Mogensen, T., \u201cTypes for 0, 1 or many uses,\u201d in Implementation of Functional Languages, LNCS 1467, pp. 112\u2013122, 1998.","DOI":"10.1007\/BFb0055427"},{"key":"38_CR22","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K. and Glew, N., \u201cFrom system f to typed assembly language,\u201d ACM Transactions on Programming Languages and Systems, 21(3), pp. 528\u2013569, May 1999.","DOI":"10.1145\/319301.319345"},{"key":"38_CR23","doi-asserted-by":"crossref","unstructured":"Necula, G.C., \u201cProof-carrying code,\u201d in Proc. of the 24 th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL \u201997), pp. 106\u2013119, Paris, January 1997.","DOI":"10.1145\/263699.263712"},{"key":"38_CR24","unstructured":"Permandla, P. and Boyapati, C., \u201cA type system for preventing data races and deadlocks in the Java virtual machine language,\u201d Technical Report."},{"issue":"1","key":"38_CR25","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/314602.314606","volume":"21","author":"R. Stata","year":"1999","unstructured":"Stata, R. and Abadi, M., \u201cA type system for Java bytecode subroutines,\u201d ACM Transactions on Programming Languages and Systems, 21(1), pp. 90\u2013137, 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"38_CR26","first-page":"55","volume":"16","author":"E. Sumii","year":"1998","unstructured":"Sumii, E. and Kobayashi, N., \u201cA generalized deadlock-free process calculus,\u201d in Proc. of Workshop on High-Level Concurrent Language (HLCL\u201998), ENTCS, 16(3), pp. 55\u201377, 1998.","journal-title":"Proc. of Workshop on High-Level Concurrent Language (HLCL\u201998), ENTCS"}],"container-title":["New Generation Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00354-008-0038-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00354-008-0038-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00354-008-0038-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T14:27:49Z","timestamp":1559053669000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00354-008-0038-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,2]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["38"],"URL":"https:\/\/doi.org\/10.1007\/s00354-008-0038-8","relation":{},"ISSN":["0288-3635","1882-7055"],"issn-type":[{"value":"0288-3635","type":"print"},{"value":"1882-7055","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,2]]}}}