{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:55:14Z","timestamp":1743054914561,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642020018"},{"type":"electronic","value":"9783642020025"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02002-5_10","type":"book-chapter","created":{"date-parts":[[2009,5,13]],"date-time":"2009-05-13T12:20:10Z","timestamp":1242217210000},"page":"181-197","source":"Crossref","is-referenced-by-count":3,"title":["Writing an OS Kernel in a Strictly and Statically Typed Language"],"prefix":"10.1007","author":[{"given":"Toshiyuki","family":"Maeda","sequence":"first","affiliation":[]},{"given":"Akinori","family":"Yonezawa","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","volume-title":"The Java Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)","edition":"3"},{"key":"10_CR2","unstructured":"ECMA: ECMA-334: C# Language Specification (2002)"},{"issue":"5","key":"10_CR3","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"10_CR4","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1145\/1189256.1189259","volume":"24","author":"J. Yang","year":"2006","unstructured":"Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. ACM Trans. Comput. Syst.\u00a024(4), 393\u2013423 (2006)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"11","key":"10_CR5","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R.: Kit: A study in operating system verification. IEEE Trans. Softw. Eng.\u00a015(11), 1382\u20131396 (1989)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-44557-9_5","volume-title":"Types for Proofs and Programs","author":"G. Betarte","year":"2000","unstructured":"Betarte, G., Cornes, C., Szasz, N., Tasistro, A.: Specification of a smart card operating system. In: Coquand, T., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 77\u201393. Springer, Heidelberg (2000)"},{"issue":"3","key":"10_CR7","doi-asserted-by":"publisher","first-page":"527","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 Trans. Program. Lang. Syst.\u00a021(3), 527\u2013568 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-46425-5_24","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D., Morrisett, J.G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, pp. 366\u2013381. Springer, Heidelberg (2000)"},{"key":"10_CR9","unstructured":"Maeda, T., Yonezawa, A.: Writing practical memory management code with a strictly typed assembly language. In: SPACE 2006: Workshop on Semantics, Program Analysis, and Computing Environments For Memory Management, pp. 35\u201346 (2006)"},{"key":"10_CR10","unstructured":"Maeda, T.: Writing an Operating System with a Strictly Typed Assembly Language. Ph.D thesis, University of Tokyo (2006)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-76929-3_3","volume-title":"Advances in Computer Science \u2013 ASIAN 2007. Computer and Network Security","author":"T. Kosakai","year":"2007","unstructured":"Kosakai, T., Maeda, T., Yonezawa, A.: Compiling C programs into a strongly typed assembly language. In: Cervesato, I. (ed.) ASIAN 2007. LNCS, vol.\u00a04846, pp. 17\u201332. Springer, Heidelberg (2007)"},{"key":"10_CR12","unstructured":"Intel Corporation: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual"},{"key":"10_CR13","unstructured":"Maeda, T.: TALK project, \n                    \n                      http:\/\/www.yl.is.s.u-tokyo.ac.jp\/~tosh\/talk\/"},{"key":"10_CR14","unstructured":"Accetta, M.J., Baron, R.V., Bolosky, W.J., Golub, D.B., Rashid, R.F., Tevanian, A., Young, M.: Mach: A new kernel foundation for UNIX development. In: USENIX, pp. 93\u2013113 (Summer 1986)"},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1145\/224056.224076","volume-title":"SOSP 1995: Proceedings of the fifteenth ACM symposium on Operating systems principles","author":"D.R. Engler","year":"1995","unstructured":"Engler, D.R., Kaashoek, M.F., O\u2019Toole Jr., J.: Exokernel: an operating system architecture for application-level resource management. In: SOSP 1995: Proceedings of the fifteenth ACM symposium on Operating systems principles, pp. 251\u2013266. ACM, New York (1995)"},{"issue":"5","key":"10_CR16","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/224057.224075","volume":"29","author":"J. Liedtke","year":"1995","unstructured":"Liedtke, J.: On \u03bc-kernel construction. SIGOPS Oper. Syst. Rev.\u00a029(5), 237\u2013250 (1995)","journal-title":"SIGOPS Oper. Syst. Rev."},{"issue":"5","key":"10_CR17","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1145\/635506.605429","volume":"30","author":"E. Witchel","year":"2002","unstructured":"Witchel, E., Cates, J., Asanovi\u0107, K.: Mondrian memory protection. SIGARCH Comput. Archit. News\u00a030(5), 304\u2013316 (2002)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"10_CR18","first-page":"331","volume-title":"POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"A. Igarashi","year":"2002","unstructured":"Igarashi, A., Kobayashi, N.: Resource usage analysis. In: POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 331\u2013342. ACM, New York (2002)"},{"issue":"1","key":"10_CR19","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/371455.371458","volume":"35","author":"M.Y. Zhu","year":"2001","unstructured":"Zhu, M.Y., Luo, L., Xiong, G.Z.: A provably correct operating system: \u03b4-core. SIGOPS Oper. Syst. Rev.\u00a035(1), 17\u201333 (2001)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"10_CR20","unstructured":"Tuch, H., Klein, G., Heiser, G.: OS verification \u2014 now! In: HOTOS 2005: Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Berkeley, CA, USA, pp. 7\u201312. USENIX Association (2005)"},{"issue":"4","key":"10_CR21","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J. McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM\u00a03(4), 184\u2013195 (1960)","journal-title":"Commun. ACM"},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1145\/224056.224077","volume-title":"SOSP 1995: Proceedings of the fifteenth ACM symposium on Operating systems principles","author":"B.N. Bershad","year":"1995","unstructured":"Bershad, B.N., Savage, S., Pardyak, P., Sirer, E.G., Fiuczynski, M.E., Becker, D., Chambers, C., Eggers, S.: Extensibility safety and performance in the SPIN operating system. In: SOSP 1995: Proceedings of the fifteenth ACM symposium on Operating systems principles, pp. 267\u2013283. ACM, New York (1995)"},{"volume-title":"System Programming in Modula-3","year":"1991","key":"10_CR23","unstructured":"Nelson, G. (ed.): System Programming in Modula-3. Prentice Hall, Englewood Cliffs (1991)"},{"key":"10_CR24","unstructured":"Hunt, G., Larus, J.R., Abadi, M., Aiken, M., Barham, P., F\u00e4hndrich, M., Hawblitzel, C., Hodson, O., Levi, S., Murphy, N., Steensgaard, B., Tarditi, D., Wobber, T., Zill, B.D.: An overview of the Singularity project. Technical Report MSR-TR-2005-135, Microsoft Research (2005)"},{"issue":"2","key":"10_CR25","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/1243418.1243424","volume":"41","author":"G.C. Hunt","year":"2007","unstructured":"Hunt, G.C., Larus, J.R.: Singularity: rethinking the software stack. SIGOPS Oper. Syst. Rev.\u00a041(2), 37\u201349 (2007)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"10_CR26","unstructured":"Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: A safe dialect of C. In: ATEC 2002: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, Berkeley, CA, USA, pp. 275\u2013288. USENIX Association (2002)"},{"issue":"1-3","key":"10_CR27","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0167-6423(97)00030-0","volume":"32","author":"G. Smith","year":"1998","unstructured":"Smith, G., Volpano, D.: A sound polymorphic type system for a dialect of C. Sci. Comput. Program.\u00a032(1-3), 49\u201372 (1998)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"10_CR28","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1145\/1065887.1065892","volume":"27","author":"G.C. Necula","year":"2005","unstructured":"Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst.\u00a027(3), 477\u2013526 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"10_CR29","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/1323293.1294295","volume":"41","author":"J. Criswell","year":"2007","unstructured":"Criswell, J., Lenharth, A., Dhurjati, D., Adve, V.: Secure virtual architecture: a safe execution environment for commodity operating systems. SIGOPS Oper. Syst. Rev.\u00a041(6), 351\u2013366 (2007)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"10_CR30","unstructured":"Dhurjati, D., Kowshik, S., Adve, V.: Enforcing Alias Analysis for Weakly Typed Languages. Technical Report\u00a0#UIUCDCS-R-2005-2657, Computer Science Dept., Univ. of Illinois (November 2005)"},{"issue":"1","key":"10_CR31","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/1053271.1053275","volume":"4","author":"D. Dhurjati","year":"2005","unstructured":"Dhurjati, D., Kowshik, S., Adve, V., Lattner, C.: Memory safety without garbage collection for embedded applications. Trans. on Embedded Computing Sys.\u00a04(1), 73\u2013111 (2005)","journal-title":"Trans. on Embedded Computing Sys."},{"issue":"6","key":"10_CR32","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/1133255.1133999","volume":"41","author":"D. Dhurjati","year":"2006","unstructured":"Dhurjati, D., Kowshik, S., Adve, V.: SAFECode: enforcing alias analysis for weakly typed languages. SIGPLAN Not.\u00a041(6), 144\u2013157 (2006)","journal-title":"SIGPLAN Not."},{"key":"10_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/224164.224168","volume-title":"FPCA 1995: Proceedings of the seventh international conference on Functional programming languages and computer architecture","author":"D.N. Turner","year":"1995","unstructured":"Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: FPCA 1995: Proceedings of the seventh international conference on Functional programming languages and computer architecture, pp. 1\u201311. ACM, New York (1995)"},{"key":"10_CR34","unstructured":"Cheney, J., Morrisett, G.: A linearly typed assembly language. Technical report, Department of Computer Science, Cornell University (2003)"},{"issue":"3-4","key":"10_CR35","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. J. Autom. Reason.\u00a031(3-4), 261\u2013302 (2003)","journal-title":"J. Autom. Reason."},{"key":"10_CR36","unstructured":"Hawblitzel, C., Wei, E., Huang, H., Krupski, E., Wittie, L.: Low-level linear memory management. In: SPACE 2004: Workshop on Semantics, Program Analysis, and Computing Environments For Memory Management. (2004)"},{"key":"10_CR37","unstructured":"Maeda, T.: TOS project, \n                    \n                      http:\/\/www.yl.is.s.u-tokyo.ac.jp\/~tosh\/tos\/"},{"key":"10_CR38","unstructured":"Maeda, T., Yonezawa, A.: Typed assembly language with interrupts (in Japanese). In: JSSST Dependable System Workshop 2007, pp. 107\u2013110 (2007)"},{"key":"10_CR39","unstructured":"Maeda, T., Yonezawa, A.: Typed assembly language for SMP (in Japanese). In: JSSST Dependable System Workshop 2008, pp. 115\u2013126 (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal to Practical Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02002-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,10,12]],"date-time":"2018-10-12T03:35:13Z","timestamp":1539315313000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02002-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642020018","9783642020025"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02002-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}