乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:29:24Z","timestamp":1707521364871},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"5","funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-09-1-0110"],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2011,11]]},"abstract":"Behavioral software contracts have become a popular mechanism for specifying and ensuring logical claims about a program's flow of values. While contracts for first-order functions come with a natural interpretation and are well understood, the various incarnations of higher-order contracts adopt, implicitly or explicitly, different views concerning the meaning of contract satisfaction. In this article, we define various notions of contract satisfaction in terms of observational equivalence and compare them with each other and notions in the literature. Specifically, we introduce a small model language with higher-order contracts and use it to formalize different notions of contract satisfaction. Each of them demands that the contract parties satisfy certain observational equivalences.<\/jats:p>","DOI":"10.1145\/2039346.2039348","type":"journal-article","created":{"date-parts":[[2011,11,21]],"date-time":"2011-11-21T19:54:36Z","timestamp":1321905276000},"page":"1-29","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["On contract satisfaction in a higher-order world"],"prefix":"10.1145","volume":"33","author":[{"given":"Christos","family":"Dimoulas","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, MA"}]},{"given":"Matthias","family":"Felleisen","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, MA"}]}],"member":"320","published-online":{"date-parts":[[2011,11,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.774917"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005971"},{"key":"e_1_2_1_5_1","volume-title":"Preproceedings of the 6th Symposium on Software Composition. 34--50","author":"Bravetti M."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11841197_10"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328471"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_15"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157896.2157898"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.07.006"},{"key":"e_1_2_1_12_1","unstructured":"Detlefs D. L. Leino K. R. M. Nelson G. and Saxe J. B. 1998. Extended static checking. Tech. rep. 158 Compaq SRC Research Report. Detlefs D. L. Leino K. R. M. Nelson G. and Saxe J. B. 1998. Extended static checking. Tech. rep. 158 Compaq SRC Research Report."},{"key":"e_1_2_1_13_1","unstructured":"Felleisen M. Findler R. B. and Flatt M. 2009. Semantics Engineering with PLT Redex. MIT Press. Felleisen M. Findler R. B. and Flatt M. 2009. Semantics Engineering with PLT Redex. MIT Press."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_16"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_1_16_1","unstructured":"Findler R. B. Felleisen M. and Blume M. 2004. An investigation of contracts as projections. Tech. rep. TR-2004-02 Computer Science Department University of Chicago. Findler R. B. Felleisen M. and Blume M. 2004. An investigation of contracts as projections. Tech. rep. TR-2004-02 Computer Science Department University of Chicago."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85373-2_7"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503240"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_20_1","volume-title":"Reference: Racket. Tech. rep. PLT-TR-2010-1","author":"Flatt M.","year":"2010"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 8th Symposium on Trends in Functional Programming (TFP). 54--69","author":"Gronski J."},{"key":"e_1_2_1_23_1","unstructured":"Hennessy M. 1988. Algebraic Theory of Processes. MIT Press. Hennessy M. 1988. Algebraic Theory of Processes. MIT Press."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_15"},{"key":"e_1_2_1_25_1","volume-title":"SAGE: Unified hybrid checking for first-class types, general refinement types, and dynamic","author":"Knowles K.","year":"2006"},{"key":"e_1_2_1_26_1","unstructured":"Koutavas V. 2008. Reasoning about imperative and higher-order programs. Ph.D. thesis Northeastern University. Koutavas V. 2008. Reasoning about imperative and higher-order programs. Ph.D. thesis Northeastern University."},{"key":"e_1_2_1_27_1","unstructured":"Meyer B. 1988. Object-oriented Software Construction. Prentice-Hall. Meyer B. 1988. Object-oriented Software Construction. Prentice-Hall."},{"key":"e_1_2_1_28_1","volume-title":"Advances in Object-Oriented Software Engineering","author":"Meyer B."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/129093"},{"key":"e_1_2_1_31_1","unstructured":"Morris J. H. 1968. Lambda-calculus models of programming languages. Ph.D. thesis Massachusetts Institute of Technology. Morris J. H. 1968. Lambda-calculus models of programming languages. Ph.D. thesis Massachusetts Institute of Technology."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.341844"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2039346.2039348","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T20:00:12Z","timestamp":1672344012000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2039346.2039348"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":37,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["10.1145\/2039346.2039348"],"URL":"https:\/\/doi.org\/10.1145\/2039346.2039348","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11]]},"assertion":[{"value":"2010-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-11-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}