乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,25]],"date-time":"2024-03-25T04:59:35Z","timestamp":1711342775740},"reference-count":31,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2016,9,22]],"date-time":"2016-09-22T00:00:00Z","timestamp":1474502400000},"content-version":"unspecified","delay-in-days":265,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2016]]},"abstract":"Abstract<\/jats:title>Effect systems have the potential to help software developers, but their practical adoption has been very limited. We conjecture that this limited adoption is due in part to the difficulty of transitioning from a system where effects are implicit and unrestricted to a system with a static effect discipline, which must settle for conservative checking in order to be decidable. To address this hindrance, we develop a theory of gradual effect checking, which makes it possible to incrementally annotate and statically check effects, while still rejecting statically inconsistent programs. We extend the generic type-and-effect framework of Marino and Millstein with a notion of unknown effects, which turns out to be significantly more subtle than unknown types in traditional gradual typing. We appeal to abstract interpretation to develop and validate the concepts of gradual effect checking. We also demonstrate how an effect system formulated in the framework of Marino and Millstein can be automatically extended to support gradual checking. We use gradual effect checking to develop a fully gradual type-and-effect framework, which permits interaction between static and dynamic checking for both effects and types.<\/jats:p>","DOI":"10.1017\/s0956796816000162","type":"journal-article","created":{"date-parts":[[2016,9,22]],"date-time":"2016-09-22T04:38:47Z","timestamp":1474519127000},"source":"Crossref","is-referenced-by-count":12,"title":["Gradual type-and-effect systems"],"prefix":"10.1017","volume":"26","author":[{"given":"FELIPE","family":"BA\u00d1ADOS SCHWERTER","sequence":"first","affiliation":[]},{"given":"RONALD","family":"GARCIA","sequence":"additional","affiliation":[]},{"given":"\u00c9RIC","family":"TANTER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"S0956796816000162_ref28","volume-title":"Programming Languages and Systems","author":"Thiemann","year":"2014"},{"key":"S0956796816000162_ref8","unstructured":"Disney T. & Flanagan C. (2011) Gradual information flow typing. In International Workshop on Scripts to Programs (STOP 2011), Co-Located with POPL 2011. Url: https:\/\/users.soe.ucsc.edu\/~cormac\/papers\/stop11.pdf."},{"key":"S0956796816000162_ref21","doi-asserted-by":"crossref","unstructured":"Rytz L. , Odersky M. & Haller P. (2012) Lightweight polymorphic effects. In Proceedings of the 26th European Conference on Object-oriented Programming (ECOOP 2012). Berlin, Germany: Springer-Verlag, pp. 258\u2013282.","DOI":"10.1007\/978-3-642-31057-7_13"},{"key":"S0956796816000162_ref26","doi-asserted-by":"crossref","unstructured":"Takikawa A. , Strickland T. S. , Dimoulas C. , Tobin-Hochstadt S. & Felleisen M. (2012) Gradual typing for first-class classes. In Proceedings of the 27th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2012). New York, NY, USA: ACM Press, pp. 793\u2013810.","DOI":"10.1145\/2384616.2384674"},{"key":"S0956796816000162_ref20","doi-asserted-by":"crossref","unstructured":"Rytz L. , Amin N. & Odersky M. (2013) A flow-insensitive, modular effect system for purity. In Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs. New York, NY, USA: ACM Press, pp. 4:1\u20134:7.","DOI":"10.1145\/2489804.2489808"},{"key":"S0956796816000162_ref7","doi-asserted-by":"crossref","unstructured":"Delaware B. , Keuchel S. , Schrijvers T. & Oliveira B. C.d.S. (2013) Modular monadic meta-theory. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013). New York, NY, USA: ACM Press, pp. 319\u2013330.","DOI":"10.1145\/2500365.2500587"},{"key":"S0956796816000162_ref12","doi-asserted-by":"crossref","unstructured":"Garcia R. , Clark A. M. & Tanter \u00c9. (2016) Abstracting gradual typing. In Proceedings of the 43rd Annual ACM Sigplan-Sigact Symposium on Principles of Programming Languages (POPL 2016). New York, NY, USA: ACM Press, pp. 429\u2013442.","DOI":"10.1145\/2837614.2837670"},{"key":"S0956796816000162_ref29","doi-asserted-by":"crossref","unstructured":"Toro M. & Tanter \u00c9. (2015) Customizable gradual polymorphic effects for scala. In Submission to the 30th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2015), New York, NY, USA: ACM Press.","DOI":"10.1145\/2814270.2814315"},{"key":"S0956796816000162_ref1","doi-asserted-by":"crossref","unstructured":"Abadi M. , Birrell A. , Harris T. & Isard M. (2008) Semantics of transactional memory and automatic mutual exclusion. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008). New York, NY, USA: ACM Press, pp. 63\u201374.","DOI":"10.1145\/1328438.1328449"},{"key":"S0956796816000162_ref23","unstructured":"Sergey I. & Clarke D. (2012) Gradual ownership types. In Proceedings of the 21st European Symposium on Programming Languages and Systems (ESOP 2012). Berlin, Germany: Springer-Verlag, pp. 579\u2013599."},{"key":"S0956796816000162_ref5","doi-asserted-by":"crossref","unstructured":"Cousot P. & Cousot R. (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL 1977). New York, NY, USA: ACM Press, pp. 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"S0956796816000162_ref3","doi-asserted-by":"crossref","unstructured":"Ba\u00f1ados Schwerter F. , Garcia R. & Tanter \u00c9. (2014) A theory of gradual effect systems. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP 2014). New York, NY, USA: ACM Press, pp. 283\u2013295.","DOI":"10.1145\/2628136.2628149"},{"key":"S0956796816000162_ref30","doi-asserted-by":"crossref","unstructured":"Wolff R. , Garcia R. , Tanter \u00c9. & Aldrich J. (2011) Gradual typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP 2011). Berlin, Germany: Springer-Verlag, pp. 459\u2013483.","DOI":"10.1007\/978-3-642-22655-7_22"},{"key":"S0956796816000162_ref27","doi-asserted-by":"crossref","unstructured":"Tang Y. M. & Jouvelot P. (1995) Effect systems with subtyping. In Proceedings of the 1995 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM 1995). New York, NY, USA: ACM Press, pp. 45\u201353.","DOI":"10.1145\/215465.215552"},{"key":"S0956796816000162_ref24","unstructured":"Siek J. & Taha W. (2007) Gradual typing for objects. In Proceedings of the 21st European Conference on Object-oriented Programming (ECOOP 2007). Berlin, Germany: Springer-Verlag, pp. 2\u201327."},{"key":"S0956796816000162_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.09.005"},{"key":"S0956796816000162_ref19","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0956796816000162_ref14","unstructured":"Gifford D. K. & Lucassen J. M. (1986) Integrating functional and imperative programming. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming. New York, NY, USA: ACM Press, pp. 28\u201338."},{"key":"S0956796816000162_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"S0956796816000162_ref9","doi-asserted-by":"crossref","unstructured":"Disney T. , Flanagan C. & McCarthy J. (2011) Temporal higher-order contracts. In Proceedings of the 16th ACM SIGPLAN Conference on Functional Programming (ICFP 2011). New York, NY, USA: ACM Press, pp. 176\u2013188.","DOI":"10.1145\/2034773.2034800"},{"key":"S0956796816000162_ref31","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796816000162_ref11","unstructured":"Findler R. B. & Felleisen M. (2002) Contracts for higher-order functions. In Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming (ICFP 2002). New York, NY, USA: ACM Press, pp. 48\u201359."},{"key":"S0956796816000162_ref4","unstructured":"Benton N. & Buchlovsky P. (2007) Semantics of an effect analysis for exceptions. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI 2007). New York, NY, USA: ACM Press, pp. 15\u201326."},{"key":"S0956796816000162_ref6","doi-asserted-by":"crossref","unstructured":"Cousot P. & Cousot R. (1979) Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1979). New York, NY, USA: ACM Press, pp. 269\u2013282.","DOI":"10.1145\/567752.567778"},{"key":"S0956796816000162_ref16","volume-title":"The Java Language Specification","author":"Gosling","year":"2003"},{"key":"S0956796816000162_ref17","unstructured":"Ina L. & Igarashi A. (2011) Gradual typing for generics. In Proceedings of the 26th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2011). New York, NY, USA: ACM Press, pp. 609\u2013624."},{"key":"S0956796816000162_ref25","unstructured":"Siek J. G. & Taha W. (2006 September) Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop, Chicago, IL, USA: University of Chicago TR-2006-06, pp. 81\u201392."},{"key":"S0956796816000162_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1119479.1119480"},{"key":"S0956796816000162_ref10","doi-asserted-by":"crossref","unstructured":"Fennell L. & Thiemann P. (2013 June) Gradual security typing with references. In Computer Security Foundations Symposium (csf), Los Alamitos, CA, USA: IEEE, pp. 224\u2013239.","DOI":"10.1109\/CSF.2013.22"},{"key":"S0956796816000162_ref15","unstructured":"Gordon C. S. , Dietl W. , Ernst M. D. & Grossman D. (2013) JavaUI: Effects for controlling UI object access. In Proceedings of the 27th European Conference on Object-oriented Programming (ECOOP 2013). Berlin, Germany: Springer-Verlag, pp. 179\u2013204."},{"key":"S0956796816000162_ref18","unstructured":"Marino D. & Millstein T. (2009) A generic type-and-effect system. In Proceedings of the ACM SIGPLAN International Workshop on Types in Language Design and Implementation, New York, NY, USA: ACM Press, pp. 39\u201350."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000162","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T19:51:00Z","timestamp":1559937060000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000162\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"references-count":31,"alternative-id":["S0956796816000162"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000162","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"article-number":"e19"}}