{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T06:59:36Z","timestamp":1794380376624,"version":"4.9.0"},"publisher-location":"London","reference-count":56,"publisher":"Springer London","isbn-type":[{"value":"9781848829114","type":"print"},{"value":"9781848829121","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-84882-912-1_4","type":"book-chapter","created":{"date-parts":[[2010,8,20]],"date-time":"2010-08-20T12:27:13Z","timestamp":1282307233000},"page":"71-99","source":"Crossref","is-referenced-by-count":3,"title":["Roles, Stacks, Histories: A Triple for Hoare"],"prefix":"10.1007","author":[{"given":"Johannes","family":"Borgstr\u00f6m","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Riccardo","family":"Pucella","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,7,21]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M.: Access control in a core calculus of dependency. In: International Conference on Functional Programming (ICFP\u201906), pp. 263\u2013273 (2006).","DOI":"10.1145\/1159803.1159839"},{"key":"4_CR2","unstructured":"Abadi, M., Fournet, C.: Access control based on execution history. In: Network and Distributed System Security Symposium (NDSS\u201903), pp. 107\u2013121. The Internet Society, ISOC, Reston, VA, USA (2003)."},{"issue":"4","key":"4_CR3","doi-asserted-by":"publisher","first-page":"706","DOI":"10.1145\/155183.155225","volume":"15","author":"M Abadi","year":"1993","unstructured":"Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Trans. Programming Languages Systems 15(4), 706\u2013734 (1993).","journal-title":"ACM Trans. Programming Languages Systems"},{"issue":"1\u20132","key":"4_CR4","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/S0304-3975(00)00175-4","volume":"266","author":"D Aspinall","year":"2001","unstructured":"Aspinall, D., Compagnoni, A.: Subtyping dependent types. Theoret. Comput Sci. 266(1\u20132), 273\u2013309 (2001).","journal-title":"Theoret. Comput Sci."},{"key":"4_CR5","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1017\/S095679680900728X","volume":"19","author":"R Atkey","year":"2009","unstructured":"Atkey, R.: Parameterized notions of computation. J. Funct. Programm. 19, 355\u2013376 (2009).","journal-title":"J. Funct. Programm."},{"key":"4_CR6","unstructured":"Banerjee, A., Naumann, D.: History-based access control and secure information flow. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), vol. 3362 of LNCS, pp. 27\u201348 Springer, Heidelberg, Germany (2005)."},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.: Stack-based access control and secure information flow. J. Funct. Programm. 15(2), 131\u2013177 (2005)","journal-title":"J. Funct. Programm."},{"key":"4_CR8","unstructured":"Becker, M.Y., Nanz, S.: A logic for state-modifying authorization policies. In: European Symposium on Research in Computer Security (ESORICS\u201907), vol. 4734 of LNCS, pp. 203\u2013218. Springer, Heidelberg, Germany (2007)."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Becker, M.Y., Sewell, P.: Cassandra: flexible trust management, applied to electronic health records. In: 17th IEEE Computer Security Foundations Workshop (CSFW\u201904), pp. 139\u2013154 (June 2004).","DOI":"10.1109\/CSFW.2004.1310738"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. Technical Report MSR-TR-2008-118, Microsoft Research (2008). Apreliminary, abridged version appears in the proceedings of CSF\u201908.","DOI":"10.1109\/CSF.2008.27"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Besson, F., Blanc, T., Fournet, C., Gordon, A.D.: From stack inspection to access control: Asecurity analysis for libraries. In: Computer Security Foundations Workshop (CSFW\u201904), pp.61\u201377 (2004).","DOI":"10.1109\/CSFW.2004.1310732"},{"key":"4_CR12","unstructured":"Borgstr\u00f6m, J., Gordon, A.D., Pucella, R.: Roles, stacks, histories: A triple for Hoare. Technical Report MSR-TR-2009-97, Microsoft Research (2009)."},{"key":"4_CR13","unstructured":"Cardelli, L.: Typechecking dependent types and subtypes. In: Foundations of Logic and Functional Programming, vol. 306 of LNCS, pp. 45\u201357. Springer (1986)."},{"key":"4_CR14","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., etal.: Implementing Mathematicswith the Nuprl Proof Development System. Prentice-Hall, Hemel Hampstead, England (1986)."},{"key":"4_CR15","unstructured":"deMoura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908), vol. 4963 of LNCS, pp. 337\u2013340. Springer (2008)."},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Programming Language Design and Implementation (PLDI\u201901), pp. 59\u201369 (2001).","DOI":"10.1145\/381694.378811"},{"issue":"3","key":"4_CR17","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J.ACM 52(3): 365\u2013473 (2005).","journal-title":"J. ACM"},{"key":"4_CR18","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver. Available at http:\/\/yices.csl.sri.com\/tool-paper.pdf , 2006."},{"key":"4_CR19","unstructured":"Ferraiolo, D.F., Kuhn, D.R.: Role based access control. In: Proc.National Computer Security Conference, pp. 554\u2013563 (1992)."},{"key":"4_CR20","unstructured":"Filli\u00e2tre, J., March\u00e9, C.: Multi-prover Verification of C Programs. In: International Conference on Formal Engineering Methods (ICFEM 2004), vol. 3308 of LNCS, pp. 15\u201329. Springer (2004)."},{"key":"4_CR21","unstructured":"Filli\u00e2tre, J.-C.: Proof of imperative programs in type theory. In: Selected Papers from the International Workshop on Types for Proofs and Programs (TYPES \u201998), 1657, pp. 78\u201392. Springer (1999)."},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Flanagan, C.: Hybrid type checking. In: ACM Symposium on Principles of Programming Languages (POPL\u201906), pp. 245\u2013256 (2006).","DOI":"10.1145\/1111037.1111059"},{"key":"4_CR23","unstructured":"Flanagan, C., Abadi, M.: Types for safe locking. In: European Symposium on Programming (ESOP\u201999), vol. 1576 of LNCS, pp. 91\u2013108, Springer (1999)."},{"issue":"3","key":"4_CR24","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1145\/641909.641912","volume":"25","author":"C Fournet","year":"2003","unstructured":"Fournet, C., Gordon, A.D.: Stack inspection: Theory and variants. ACM Trans. Programm. Languages Systems 25(3): 360\u2013399 (2003).","journal-title":"ACM Trans. Programm. Languages Systems"},{"key":"4_CR25","unstructured":"Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. In: 14th European Symposium on Programming (ESOP\u201905), vol. 3444 of LNCS, pp. 141\u2013156. Springer, Heidelberg, Germany(2005)."},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies in distributed systems. In: 20th IEEE Computer Security Foundation Symposium (CSF\u201907), pp. 31\u201345 (2007).","DOI":"10.1109\/CSF.2007.7"},{"key":"4_CR27","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ML. In: Programming Language Design and Implementation (PLDI\u201991), pp. 268\u2013277. ACM, New York, NY, USA (1991)."},{"key":"4_CR28","unstructured":"Gifford, D., Lucassen, J.: Integrating functional and imperative programming. In: ACM Conference on Lisp and Functional Programming, pp. 28\u201338, (1986)."},{"key":"4_CR29","unstructured":"Gong, L.: Inside Java 2 Platform Security: Architecture, API Design, and Implementation. Addison-Wesley (1999)."},{"issue":"4","key":"4_CR30","doi-asserted-by":"crossref","first-page":"451","DOI":"10.3233\/JCS-2003-11402","volume":"11","author":"AD Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.S.A.: Authenticity by typing for security protocols. J. Comput. Security 11(4): 451\u2013521 (2003).","journal-title":"J. Comput. Security"},{"key":"4_CR31","unstructured":"Gronski, J., Knowles, K., Tomb, A., Freund, S.N., Flanagan, C.: Sage: hybrid checking for flexible specifications. In: R.Findler, (ed.) Scheme and Functional Programming Workshop, pp. 93\u2013104, (2006)."},{"key":"4_CR32","unstructured":"Gunter, C.: Semantics of Programming Languages. MIT, Kluwer, Dordrecht, the Netherlands (1992)."},{"key":"4_CR33","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/54289.871709","volume":"22","author":"N Hardy","year":"1988","unstructured":"Hardy, N.: The confused deputy (or why capabilities might have been invented). ACM SIGOPS Operat. Systems Rev., 22, 36\u201338 (1988).","journal-title":"ACM SIGOPS Operat. Systems Rev."},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Jia, L., Vaughan, J.A., Mazurak, K., Zhao, J., Zarko, L., Schorr, J., Zdancewic, S.: AURA: Preliminary technical results. Technical Report MS-CIS-08-10, University of Pennsylvania (2008).","DOI":"10.1145\/1411204.1411212"},{"key":"4_CR35","unstructured":"Knowles, K.W., Flanagan, C.: Type reconstruction for general refinement types. In: ESOP, vol. 4421 of LNCS, pp. 505\u2013519. Springer (2007)."},{"key":"4_CR36","unstructured":"Li, N., Mitchell, J.C., Winsborough, W.H.: Design of a role-based trust management framework. In: IEEE Security and Privacy, pp 114\u2013130, (2002)."},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Maffeis, S., Abadi, M., Fournet, C., Gordon, A.D.: Code-carrying authorization. In: European Symposium On Research In Computer Security (ESORICS\u201908), pp. 563\u2013579 (2008).","DOI":"10.1007\/978-3-540-88313-5_36"},{"key":"4_CR38","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 computations and monads. Inform. Comput., 93, 55\u201392 (1991).","journal-title":"Inform. Comput."},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare Type Theory. In: International Conference on Functional Programming (ICFP\u201906), pp. 62\u201373 (2006).","DOI":"10.1145\/1159803.1159812"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: International Conference on Functional Programming (ICFP\u201908), pp.229\u2013240 (2008).","DOI":"10.1145\/1411204.1411237"},{"key":"4_CR41","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin-L\u00f6f\u2019s Type Theory. Clarendon Press Oxford (1990)."},{"issue":"5","key":"4_CR42","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1017\/S096012950007002X","volume":"6","author":"B Pierce","year":"1996","unstructured":"Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. Math. Structures Comput. Sci., 6(5) 409\u2013454 (1996).","journal-title":"Math. Structures Comput. Sci."},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"Pistoia, M., Banerjee, A., Naumann, D.: Beyond stack inspection: A unified access-control and information-flow security model. In: IEEE Security and Privacy, pp. 149\u2013163 (2007).","DOI":"10.1109\/SP.2007.10"},{"issue":"2","key":"4_CR44","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1147\/sj.462.0265","volume":"46","author":"M Pistoia","year":"2007","unstructured":"Pistoia, M., Chandra, S., Fink, S.J., Yahav, E.: A survey of static analysis methods for identifying security vulnerabilities in software systems. IBM Syst. J. 46(2), 265\u2013288 (2007).","journal-title":"IBM Syst. J."},{"key":"4_CR45","volume-title":"Denotational semantics with partial functions","author":"GD Plotkin","year":"1985","unstructured":"Plotkin, G.D.: Denotational semantics with partial functions. Unpublished lecture notes, CSLI, Stanford University (July 1985)."},{"issue":"2","key":"4_CR46","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1145\/1057387.1057392","volume":"27","author":"F Pottier","year":"2005","unstructured":"Pottier, F., Skalka, C., Smith, S.: A systematic approach to static access control. ACM Trans. on Programm. Languages Systems 27(2), 344\u2013382 (2005).","journal-title":"ACM Trans. on Programm. Languages Systems"},{"key":"4_CR47","unstructured":"Ranise S., Tinelli, C.: The SMT-LIB Standard: Version 1.2 (2006)."},{"key":"4_CR48","unstructured":"R\u00e9gis-Gianas, Y., Pottier, F.: A Hoare logic for call-by-value functional programs. In: Mathematics of Program Construction (MPC\u201908), vol. 5133 of LNCS, pp. 305\u2013335. Springer, Heidelberg, Germany (2008)."},{"key":"4_CR49","unstructured":"Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: Programming Language Design and Implementation (PLDI\u201908), pp. 159\u2013169. ACM, New York, NY, USA (2008)."},{"issue":"9","key":"4_CR50","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Trans. Software Eng., 24(9), 709\u2013720 (1998).","journal-title":"IEEE Trans. Software Eng."},{"issue":"3\u20134","key":"4_CR51","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01019462","volume":"6","author":"A Sabry","year":"1993","unstructured":"Sabry A., Felleisen, M.: Reasoning about programs in continuation-passing style. LISP and Symbolic Comput., 6(3\u20134), 289\u2013360 (1993).","journal-title":"LISP and Symbolic Comput."},{"issue":"2","key":"4_CR52","first-page":"38","volume":"29","author":"R Sandhu","year":"1996","unstructured":"Sandhu, R., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. IEEE Comput. 29(2), 38\u201347 (1996).","journal-title":"Role-based access control models. IEEE Comput."},{"key":"4_CR53","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"RE Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng. 12, 157\u2013171 (1986).","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR54","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1017\/S0960129500001560","volume":"2","author":"P Wadler","year":"1992","unstructured":"Wadler, P.: Comprehending monads. Math. Struct. Comput. Sci. 2, 461\u2013493 (1992).","journal-title":"Math. Struct. Comput. Sci."},{"issue":"4","key":"4_CR55","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/363516.363520","volume":"9","author":"DS Wallach","year":"2000","unstructured":"Wallach, D.S., Appel, A.W., Felten, E.W.: SAFKASI: A security mechanism for language-based systems. ACM Trans. Software Eng. Methodo., 9(4), pp. 341\u2013378 (2000).","journal-title":"ACM Trans. Software Eng. Methodo."},{"key":"4_CR56","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F., Dependent types in practical programming. In: Principles of Programming Languages (POPL\u201999), pp. 214\u2013227 (1999).","DOI":"10.1145\/292540.292560"}],"container-title":["Reflections on the Work of C.A.R. Hoare"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-84882-912-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T16:09:34Z","timestamp":1740413374000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-84882-912-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781848829114","9781848829121"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-1-84882-912-1_4","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-1-84882-912-1","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010]]}}}