{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:06:47Z","timestamp":1760044007977,"version":"3.41.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"4S","license":[{"start":{"date-parts":[[2013,7,9]],"date-time":"2013-07-09T00:00:00Z","timestamp":1373328000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGPLAN Not."],"published-print":{"date-parts":[[2013,7,9]]},"abstract":"<jats:p>Assertions play an important role in the construction of robust software. Their use in programming languages dates back to the 1970s. Eiffel, an object-oriented programming language, wholeheartedly adopted assertions and developed the \"Design by Contract\" philosophy. Indeed, the entire object-oriented community recognizes the value of assertion-based contracts on methods.<\/jats:p>\n          <jats:p>In contrast, languages with higher-order functions do not support assertion-based contracts. Because predicates on functions are, in general, undecidable, specifying such predicates appears to be meaningless. Instead, the functional languages community developed type systems that statically approximate interesting predicates.<\/jats:p>\n          <jats:p>\n            In this paper, we show how to support higher-order function contracts in a theoretically well-founded and practically viable manner. Specifically, we introduce ?\n            <jats:sup>CON<\/jats:sup>\n            , a typed lambda calculus with assertions for higher-order functions. The calculus models the assertion monitoring system that we employ in Dr Scheme. We establish basic properties of the model (type soundness, etc.) and illustrate the usefulness of contract checking with examples from Dr Scheme's code base.\n          <\/jats:p>\n          <jats:p>We believe that the development of an assertion system for higherorder functions serves two purposes. On one hand, the system has strong practical potential because existing type systems simply cannot express many assertions that programmers would like to state. nOn the other hand, an inspection of a large base of invariants may provide inspiration for the direction of practical future type system research.<\/jats:p>","DOI":"10.1145\/2502508.2502521","type":"journal-article","created":{"date-parts":[[2013,7,16]],"date-time":"2013-07-16T18:06:45Z","timestamp":1373998005000},"page":"34-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["ICFP 2002"],"prefix":"10.1145","volume":"48","author":[{"given":"Robert Bruce","family":"Findler","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, Massachusetts"}]},{"given":"Matthias","family":"Felleisen","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, Massachusetts"}]}],"member":"320","published-online":{"date-parts":[[2013,7,9]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Standard ML of New Jersey","author":"Bell Labratories","year":"1993","unstructured":"AT&T Bell Labratories . Standard ML of New Jersey , 1993 . AT&T Bell Labratories. Standard ML of New Jersey, 1993."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277719"},{"key":"e_1_2_1_3_1","volume-title":"How to Design Programs","author":"Felleisen M.","year":"2001","unstructured":"Felleisen , M. , R. B. Findler , M. Flatt and S. Krishnamurthi . How to Design Programs . MIT Press , 2001 . Felleisen, M., R. B. Findler, M. Flatt and S. Krishnamurthi. How to Design Programs. MIT Press, 2001."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004208"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289432"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581486"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/645580.658808"},{"key":"e_1_2_1_11_1","volume-title":"August","author":"Gomes B.","year":"1996","unstructured":"Gomes , B. , D. Stoutamire , B. Vaysman and H. Klawitter . A Language Manual for Sather 1.1 , August 1996 . Gomes, B., D. Stoutamire, B. Vaysman and H. Klawitter. A Language Manual for Sather 1.1, August 1996."},{"key":"e_1_2_1_12_1","volume-title":"The Java\u00bf Language Specification","author":"Gosling J.","year":"1996","unstructured":"Gosling , J. , B. Joy and J. Guy Steele . The Java\u00bf Language Specification . Addison-Wesley , 1996 . Gosling, J., B. Joy and J. Guy Steele. The Java\u00bf Language Specification. Addison-Wesley, 1996."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176927"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/53580.53581"},{"key":"e_1_2_1_15_1","volume-title":"Reid and The Yale Haskell Group. The Hugs 98 User Manual","author":"Jones M. P.","year":"1999","unstructured":"Jones , M. P. , A. Reid and The Yale Haskell Group. The Hugs 98 User Manual , 1999 . Jones, M. P., A. Reid and The Yale Haskell Group. The Hugs 98 User Manual, 1999."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/290229.290234"},{"key":"e_1_2_1_17_1","volume-title":"Blue: Language Specification, version 0.94","author":"K\u00f6lling M.","year":"1997","unstructured":"K\u00f6lling , M. and J. Rosenberg . Blue: Language Specification, version 0.94 , 1997 . K\u00f6lling, M. and J. Rosenberg. Blue: Language Specification, version 0.94, 1997."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176926"},{"key":"e_1_2_1_19_1","volume-title":"The Objective Caml system, Documentation and User's guide","author":"Leroy X.","year":"1997","unstructured":"Leroy , X. The Objective Caml system, Documentation and User's guide , 1997 . Leroy, X. The Objective Caml system, Documentation and User's guide, 1997."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/533091"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.230345"},{"key":"e_1_2_1_22_1","volume-title":"Eiffel: The Language","author":"Meyer B.","year":"1992","unstructured":"Meyer , B. Eiffel: The Language . Prentice Hall , 1992 . Meyer, B. Eiffel: The Language. Prentice Hall, 1992."},{"key":"e_1_2_1_23_1","volume-title":"The Definition of Standard ML","author":"Milner R.","year":"1990","unstructured":"Milner , R. , M. Tofte and R. Harper . The Definition of Standard ML . MIT Press , 1990 . Milner, R., M. Tofte and R. Harper. The Definition of Standard ML. MIT Press, 1990."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/355602.361309"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263707"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.341844"},{"key":"e_1_2_1_28_1","volume-title":"Bigloo: A practical Scheme compiler","author":"Serrano M.","year":"1992","unstructured":"Serrano , M. Bigloo: A practical Scheme compiler , 1992 --2002. Serrano, M. Bigloo: A practical Scheme compiler, 1992--2002."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003725"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/800179.810196"},{"key":"e_1_2_1_31_1","volume-title":"Eiffel: An Introduction","author":"Switzer R.","year":"1993","unstructured":"Switzer , R. Eiffel: An Introduction . Prentice Hall , 1993 . Switzer, R. Eiffel: An Introduction. Prentice Hall, 1993."},{"key":"e_1_2_1_32_1","volume-title":"Component Software","author":"Szyperski C.","year":"1998","unstructured":"Szyperski , C. Component Software . Addison-Wesley , 1998 . Szyperski, C. Component Software. Addison-Wesley, 1998."},{"key":"e_1_2_1_33_1","volume-title":"The Glasgow Haskell Compiler User's Guide","author":"The GHC","year":"1999","unstructured":"The GHC Team. The Glasgow Haskell Compiler User's Guide , 1999 . The GHC Team. The Glasgow Haskell Compiler User's Guide, 1999."}],"container-title":["ACM SIGPLAN Notices"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502508.2502521","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2502508.2502521","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:54Z","timestamp":1750234734000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502508.2502521"}},"subtitle":["Contracts for higher-order functions"],"short-title":[],"issued":{"date-parts":[[2013,7,9]]},"references-count":31,"journal-issue":{"issue":"4S","published-print":{"date-parts":[[2013,7,9]]}},"alternative-id":["10.1145\/2502508.2502521"],"URL":"https:\/\/doi.org\/10.1145\/2502508.2502521","relation":{},"ISSN":["0362-1340","1558-1160"],"issn-type":[{"type":"print","value":"0362-1340"},{"type":"electronic","value":"1558-1160"}],"subject":[],"published":{"date-parts":[[2013,7,9]]},"assertion":[{"value":"2013-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}