{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:56:00Z","timestamp":1776891360984,"version":"3.51.2"},"reference-count":50,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"2","license":[{"start":{"date-parts":[[2008,3,1]],"date-time":"2008-03-01T00:00:00Z","timestamp":1204329600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2008,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The properties verified are based on the ordered sequence of events that occur during program execution, so-called\n                    <jats:italic>event traces<\/jats:italic>\n                    . Our type and effect systems infer conservative approximations of the event traces arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the \u03bb-calculus. Technical results include a type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the\n                    <jats:italic>trace effects<\/jats:italic>\n                    inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms. A type safety result is proven for both unification and subtyping constraint versions of the type system, ensuring that statically well-typed programs do not contain trace event checks that can fail at run-time.\n                  <\/jats:p>","DOI":"10.1017\/s0956796807006466","type":"journal-article","created":{"date-parts":[[2007,7,5]],"date-time":"2007-07-05T09:09:50Z","timestamp":1183626590000},"page":"179-249","source":"Crossref","is-referenced-by-count":44,"title":["Types and trace effects of higher order programs"],"prefix":"10.46298","volume":"18","author":[{"given":"CHRISTIAN","family":"SKALKA","sequence":"first","affiliation":[]},{"given":"SCOTT","family":"SMITH","sequence":"additional","affiliation":[]},{"given":"DAVID","family":"VAN HORN","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,3,1]]},"reference":[{"key":"S0956796807006466_manual_ref-13","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"S0956796807006466_manual_ref-18","unstructured":"Esparza, J. (1994) On the decidability of model checking for several mu-calculi and Petri nets. In Proceeding of CAAP '94. Lecture Notes in Computer Science, vol. 787."},{"key":"S0956796807006466_manual_ref-35","first-page":"30","article-title":"Enforceable security policies","volume":"3","author":"Schneider","year":"2000","journal-title":"Inform. Syst. Secur."},{"key":"S0956796807006466_manual_ref-5","first-page":"316","volume-title":"FoSSaCS","author":"Bartoletti","year":"2005"},{"key":"S0956796807006466_manual_ref-28","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944725"},{"key":"S0956796807006466_manual_ref-38","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351244"},{"key":"S0956796807006466_manual_ref-2","doi-asserted-by":"publisher","DOI":"10.1142\/p132"},{"key":"S0956796807006466_manual_ref-6","unstructured":"Bauer, L. , Ligatti, J. & Walker, D. (2002a) More enforceable security policies. In Proceedings of the Foundations of Computer Security Workshop."},{"key":"S0956796807006466_manual_ref-22","doi-asserted-by":"publisher","DOI":"10.1145\/1134744.1134748"},{"key":"S0956796807006466_manual_ref-39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"S0956796807006466_manual_ref-36","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069787"},{"key":"S0956796807006466_manual_ref-26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40018-9_15"},{"key":"S0956796807006466_manual_ref-37","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80779-5"},{"key":"S0956796807006466_manual_ref-10","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"S0956796807006466_manual_ref-30","doi-asserted-by":"publisher","DOI":"10.1145\/210184.210187"},{"key":"S0956796807006466_manual_ref-40","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.01.027"},{"key":"S0956796807006466_manual_ref-41","doi-asserted-by":"crossref","unstructured":"Steffen, B. & Burkart, O. (1992) Model checking for context-free processes. In CONCUR'92, Stony Brook (NY). Lecture Notes in Computer Science (LNCS), vol. 630. Heidelberg, Germany: Springer-Verlag, pp. 123\u2013137.","DOI":"10.1007\/BFb0084787"},{"key":"S0956796807006466_manual_ref-44","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185530"},{"key":"S0956796807006466_manual_ref-3","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_7"},{"key":"S0956796807006466_manual_ref-19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45500-0_16"},{"key":"S0956796807006466_manual_ref-25","unstructured":"Jensen, T. , M\u00e9tayer, D. Le & Thorn, T. (1999) Verification of control flow based security properties. In Proceedings of the 1999 IEEE Symposium on Security and Privacy."},{"key":"S0956796807006466_manual_ref-9","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571166"},{"key":"S0956796807006466_manual_ref-21","unstructured":"Gong, L. , Mueller, M. , Prafullchandra, H. & Schemers, R. (1997) Going beyond the sandbox: An overview of the new security architecture in the Java Development Kit 1.2. In USENIX Symposium on Internet Technologies and Systems, pp. 103\u2013112."},{"key":"S0956796807006466_manual_ref-24","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503303"},{"key":"S0956796807006466_manual_ref-4","first-page":"211","volume-title":"CSFW","author":"Bartoletti","year":"2005"},{"key":"S0956796807006466_manual_ref-14","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"S0956796807006466_manual_ref-33","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286954"},{"key":"S0956796807006466_manual_ref-42","unstructured":"Stone, C. (2000) Singleton Types and Singleton Kinds. Tech. Rept. CMU-CS-00-153. Carnegie Mellon University."},{"key":"S0956796807006466_manual_ref-8","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2001-9303"},{"key":"S0956796807006466_manual_ref-11","doi-asserted-by":"publisher","DOI":"10.1145\/586110.586142"},{"key":"S0956796807006466_manual_ref-12","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325703"},{"key":"S0956796807006466_manual_ref-32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_3"},{"key":"S0956796807006466_manual_ref-47","unstructured":"VanHorn, D. Horn, D. (2006a) Algorithmic Trace Effect Analysis. M.Phil. thesis, University of Vermont."},{"key":"S0956796807006466_manual_ref-17","doi-asserted-by":"crossref","unstructured":"Erlingsson, \u00da. & Schneider, F. B. (2000) SASI enforcement of security policies: A retrospective. In NSPW '99: Proceedings of the 1999 Workshop on New Security Paradigms, pp. 87\u201395.","DOI":"10.1145\/335169.335201"},{"key":"S0956796807006466_manual_ref-48","unstructured":"VanHorn, D. Horn, D. (2006b) Trace effect analyis, OCaml implementation. Available at: http:\/\/www.cs.uvm.edu\/dvanhorn\/trace\/. Accessed June 2007."},{"key":"S0956796807006466_manual_ref-46","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61739-6_52"},{"key":"S0956796807006466_manual_ref-49","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325728"},{"key":"S0956796807006466_manual_ref-29","doi-asserted-by":"publisher","DOI":"10.1145\/165854.167976"},{"key":"S0956796807006466_manual_ref-15","first-page":"38","volume-title":"ACM Conference on Computer and Communications Security","author":"Edjlali","year":"1998"},{"key":"S0956796807006466_manual_ref-31","first-page":"22","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0956796807006466_manual_ref-34","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007734417713"},{"key":"S0956796807006466_manual_ref-20","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512531"},{"key":"S0956796807006466_manual_ref-7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36532-X_10"},{"key":"S0956796807006466_manual_ref-45","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"S0956796807006466_manual_ref-43","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44716-4_16"},{"key":"S0956796807006466_manual_ref-1","unstructured":"Abadi, M. & Fournet, C. (2003) Access control based on execution history. In Proceedings of the 10th Annual Network and Distributed System Security Symposium (NDSS'03)."},{"key":"S0956796807006466_manual_ref-23","doi-asserted-by":"publisher","DOI":"10.1145\/1180475.1180479"},{"key":"S0956796807006466_manual_ref-16","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80008-2"},{"key":"S0956796807006466_manual_ref-27","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"S0956796807006466_manual_ref-50","unstructured":"Wallach, D. S. & Felten, E. (1998) Understanding Java stack inspection. In Proceedings of the 1998 IEEE Symposium on Security and Privacy."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006466","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:09Z","timestamp":1776889149000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006466\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["S0956796807006466"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006466","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3]]}}}