{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:04Z","timestamp":1763468104334,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642342806"},{"type":"electronic","value":"9783642342813"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34281-3_15","type":"book-chapter","created":{"date-parts":[[2012,10,29]],"date-time":"2012-10-29T18:38:09Z","timestamp":1351535889000},"page":"182-197","source":"Crossref","is-referenced-by-count":8,"title":["The Confinement Problem in the Presence of Faults"],"prefix":"10.1007","author":[{"given":"William L.","family":"Harrison","sequence":"first","affiliation":[]},{"given":"Adam","family":"Procter","sequence":"additional","affiliation":[]},{"given":"Gerard","family":"Allwein","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Banerjee, A., Heintze, N., Riecke, J.: A core calculus of dependency. In: 26th ACM Symp. on Principles of Programming Languages, pp. 147\u2013160 (1999)","DOI":"10.1145\/292540.292555"},{"key":"15_CR2","unstructured":"Allwein, G., Harrison, W.L.: Partially-ordered modalities. In: Advances in Modal Logic, pp. 1\u201321 (2010)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Barham, P., Dragovic, B., Fraser, K., Hand, S., Harris, T., Ho, A., Neugebauer, R., Pratt, I., Warfield, A.: Xen and the art of virtualization. In: Proceedings of the 19th ACM Symposium on Operating Systems Principles, pp. 164\u2013177 (2003)","DOI":"10.1145\/1165389.945462"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-31982-5_20","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Bartolett","year":"2005","unstructured":"Bartolett, M., Degano, P., Ferrari, G.-L.: History-Based Access Control with Local Policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 316\u2013332. Springer, Heidelberg (2005)"},{"key":"15_CR5","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: Types and effects for secure service orchestration. In: 19th IEEE Computer Security Foundations Workshop (2006)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-36532-X_10","volume-title":"Software Security \u2013 Theories and Systems","author":"L. Bauer","year":"2003","unstructured":"Bauer, L., Ligatti, J., Walker, D.W.: Types and Effects for Non-interfering Program Monitors. In: Okada, M., Babu, C.S., Scedrov, A., Tokuda, H. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 154\u2013171. Springer, Heidelberg (2003)"},{"key":"15_CR7","unstructured":"Benton, N., Hur, C.-K., Kennedy, A., McBride, C.: Strongly Typed Term Representations in Coq. Journal of Automated Reasoning, 1\u201319 (to appear)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Certified programming with dependent types Book draft of April 12 (2012), http:\/\/adam.chlipala.net\/cpdt\/","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure Microkernels, State Monads and Scalable Refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: Symposium on Security and Privacy, pp. 11\u201320. IEEE (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-22953-4_24","volume-title":"Fundamentals of Computation Theory","author":"S. Goncharov","year":"2011","unstructured":"Goncharov, S., Schr\u00f6der, L.: A Coinductive Calculus for Asynchronous Side-Effecting Processes. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol.\u00a06914, pp. 276\u2013287. Springer, Heidelberg (2011)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/11784180_14","volume-title":"Algebraic Methodology and Software Technology","author":"W.L. Harrison","year":"2006","unstructured":"Harrison, W.L.: The Essence of Multitasking. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 158\u2013172. Springer, Heidelberg (2006)"},{"issue":"5","key":"15_CR14","doi-asserted-by":"crossref","first-page":"599","DOI":"10.3233\/JCS-2009-0356","volume":"17","author":"W.L. Harrison","year":"2009","unstructured":"Harrison, W.L., Hook, J.: Achieving information flow security through monadic control of effects. Journal of Computer Security\u00a017(5), 599\u2013653 (2009)","journal-title":"Journal of Computer Security"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"1","key":"15_CR16","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0304-3975(96)00169-7","volume":"175","author":"S. Kobayashi","year":"1997","unstructured":"Kobayashi, S.: Monad as modality. Theor. Computer Science\u00a0175(1), 29\u201374 (1997)","journal-title":"Theor. Computer Science"},{"issue":"10","key":"15_CR17","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1145\/362375.362389","volume":"16","author":"B. Lampson","year":"1973","unstructured":"Lampson, B.: A note on the confinement problem. CACM\u00a016(10), 613\u2013615 (1973)","journal-title":"CACM"},{"key":"15_CR18","unstructured":"Liang, S.: Modular Monadic Semantics and Comp. PhD thesis, Yale Univ. (1998)"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-15497-3_8","volume-title":"Computer Security \u2013 ESORICS 2010","author":"H. Mantel","year":"2010","unstructured":"Mantel, H., Sudbrock, H.: Flexible Scheduler-Independent Security. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol.\u00a06345, pp. 116\u2013133. Springer, Heidelberg (2010)"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Martin, W., White, P., Taylor, F.S., Goldberg, A.: Formal construction of the mathematically analyzed separation kernel. In: Proceedings of the 15th IEEE International Conference on Automated Software Engineering, pp. 133\u2013141 (2000)","DOI":"10.1109\/ASE.2000.873658"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press (1997)","DOI":"10.7551\/mitpress\/2319.001.0001"},{"issue":"1","key":"15_CR22","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation\u00a093(1), 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"15_CR23","unstructured":"Nanevski, A.: A Modal Calculus for Exception Handling. In: Intuitionistic Modal Logics and Applications Workshop (IMLA 2005) (June 2005)"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis (1999)","DOI":"10.1007\/978-3-662-03811-6"},{"key":"15_CR25","unstructured":"Peyton Jones, S. (ed.): Haskell 98 Language and Libraries, the Revised Report. Cambridge University Press (2003)"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Russo, A., Sabelfeld, A.: Securing interaction between threads and the scheduler. In: Proc. of the 19th IEEE Workshop on Comp. Sec. Found., pp. 177\u2013189 (2006)","DOI":"10.1109\/CSFW.2006.29"},{"issue":"1","key":"15_CR27","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information flow security. IEEE Journal on Selected Areas in Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Swierstra, W., Altenkirch, T.: Beauty in the beast. In: Proceedings of the ACM SIGPLAN Haskell Workshop (Haskell 2007), pp. 25\u201336 (2007)","DOI":"10.1145\/1291201.1291206"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Wadler, P.: The marriage of effects and monads. In: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming, pp. 63\u201374 (1998)","DOI":"10.1145\/291251.289429"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34281-3_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,19]],"date-time":"2025-04-19T21:24:30Z","timestamp":1745097870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34281-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642342806","9783642342813"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34281-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}