{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T00:42:06Z","timestamp":1790988126477,"version":"4.1.0"},"reference-count":62,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T00:00:00Z","timestamp":1702425600000},"content-version":"unspecified","delay-in-days":346,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Behavioral software contracts allow programmers to strengthen the obligations and promises that they express with conventional types. They lack expressive power, though, when it comes to invariants that hold across several function calls. Trace contracts narrow this expressiveness gap. A trace contract is a predicate over the sequence of values that flow through function calls and returns. This paper presents a principled design, an implementation, and an evaluation of trace contracts.<\/jats:p>","DOI":"10.1017\/s0956796823000096","type":"journal-article","created":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T04:56:54Z","timestamp":1702443414000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":7,"title":["Trace contracts"],"prefix":"10.1017","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4384-6351","authenticated-orcid":false,"given":"CAMERON","family":"MOY","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6678-1004","authenticated-orcid":false,"given":"MATTHIAS","family":"FELLEISEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2023,12,13]]},"reference":[{"key":"S0956796823000096_ref34","doi-asserted-by":"crossref","unstructured":"Kiczales, G. , Lamping, J. , Mendhekar, A. , Maeda, C. , Lopes, C. , Loingtier, J.-M. & Irwin, J. (1997) Aspect-oriented programming. In European Conference on Object-Oriented Programming (ECOOP).","DOI":"10.1007\/BFb0053381"},{"key":"S0956796823000096_ref49","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1016\/j.scico.2013.09.005","article-title":"Computational contracts","volume":"98","author":"Scholliers","year":"2015","journal-title":"Science of Computer Programming."},{"key":"S0956796823000096_ref8","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/2.774917","article-title":"Making components contract aware","volume":"32","author":"Beugnard","year":"1999","journal-title":"Computer."},{"key":"S0956796823000096_ref21","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1145\/3127323","article-title":"A programmable programming language","volume":"61","author":"Felleisen","year":"2018","journal-title":"Commun. ACM (CACM)."},{"key":"S0956796823000096_ref11","doi-asserted-by":"crossref","unstructured":"Chen, F. , d\u2019Amorim, M. & Ro\u015fu, G. (2005) Checking and correcting behaviors of Java programs at runtime with Java-MOP. In Workshop on Runtime Verification (RV).","DOI":"10.1016\/j.entcs.2006.02.002"},{"key":"S0956796823000096_ref20","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0167-6423(91)90036-W","article-title":"On the expressive power of programming languages","volume":"17","author":"Felleisen","year":"1991","journal-title":"Sci. Comput. Program."},{"key":"S0956796823000096_ref35","doi-asserted-by":"crossref","unstructured":"Koskinen, E. & Terauchi, T. (2014) Local temporal reasoning. In Logic in Computer Science (LICS).","DOI":"10.1145\/2603088.2603138"},{"key":"S0956796823000096_ref18","doi-asserted-by":"crossref","unstructured":"Dimoulas, C. , Tobin-Hochstadt, S. & Felleisen, M. (2012) Complete monitors for behavioral contracts. In European Symposium on Programming (ESOP).","DOI":"10.1007\/978-3-642-28869-2_11"},{"key":"S0956796823000096_ref37","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","article-title":"A brief account of runtime verification","volume":"78","author":"Leucker","year":"2009","journal-title":"J. Logic Algebr. Program."},{"key":"S0956796823000096_ref45","volume-title":"Principles of Program Analysis","author":"Nielson","year":"2005"},{"key":"S0956796823000096_ref62","doi-asserted-by":"crossref","unstructured":"Xiang, C. , Qi, Z. & Binder, W. (2015) Flexible and extensible runtime verification for Java. Int. J. Softw. Eng. Knowl. Eng. 25(9), 1595\u20131609.","DOI":"10.1142\/S0218194015400343"},{"key":"S0956796823000096_ref1","doi-asserted-by":"crossref","unstructured":"Andersen, L. , Ballantyne, M. & Felleisen, M. (2020) Adding interactive visual syntax to textual code. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA).","DOI":"10.1145\/3428290"},{"key":"S0956796823000096_ref26","doi-asserted-by":"crossref","unstructured":"Gay, S. J. , Vasconcelos, V. T. , Ravara, A. , Gesbert, N. & Caldeira, A. Z. (2010) Modular session types for distributed object-oriented programming. In Principles of Programming Languages (POPL).","DOI":"10.1145\/1706299.1706335"},{"key":"S0956796823000096_ref38","unstructured":"McCarthy, J. (2011) Automata: Compiling State Machines. Available at: https:\/\/docs.racket-lang.org\/automata\/index.html"},{"key":"S0956796823000096_ref17","doi-asserted-by":"crossref","unstructured":"Dimoulas, C. , New, M. S. , Findler, R. B. & Felleisen, M. (2016) Oh lord, please don\u2019t let contracts be misunderstood (Functional Pearl). In International Conference on Functional Programming (ICFP).","DOI":"10.1145\/2951913.2951930"},{"key":"S0956796823000096_ref39","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","article-title":"An Overview of the MOP runtime verification framework","volume":"14","author":"Meredith","year":"2011","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"S0956796823000096_ref48","doi-asserted-by":"crossref","unstructured":"Pucella, R. & Tov, J. A. (2008) Haskell session types with (almost) no class. In Haskell Symposium.","DOI":"10.1145\/1411286.1411290"},{"key":"S0956796823000096_ref60","doi-asserted-by":"crossref","unstructured":"Waye, L. , Chong, S. & Dimoulas, C. (2017) Whip: Higher-order contracts for modern services. In International Conference on Functional Programming (ICFP).","DOI":"10.1145\/3110280"},{"key":"S0956796823000096_ref58","unstructured":"Toronto, N. & Hars\u00e1nyi, A. (2011) Plot: Graph plotting. Available at: https:\/\/docs.racket-lang.org\/plot\/index.html."},{"key":"S0956796823000096_ref14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2039346.2039348","article-title":"On contract satisfaction in a higher-order world","volume":"33","author":"Dimoulas","year":"2011","journal-title":"Trans. Program. Lang. Syst. (TOPLAS)."},{"key":"S0956796823000096_ref2","first-page":"1","article-title":"Feature-specific profiling","volume":"41","author":"Andersen","year":"2018","journal-title":"Trans. Program. Lang. Syst. (TOPLAS)."},{"key":"S0956796823000096_ref23","doi-asserted-by":"crossref","unstructured":"Findler, R. B. & Felleisen, M. (2002) Contracts for higher-order functions. In International Conference on Functional Programming (ICFP).","DOI":"10.1145\/581478.581484"},{"key":"S0956796823000096_ref46","unstructured":"Owens, Z. (2012) Contract monitoring as an effect. In Higher-Order Programming with Effects (HOPE)."},{"key":"S0956796823000096_ref40","author":"Meyer","year":"1988"},{"key":"S0956796823000096_ref57","doi-asserted-by":"crossref","unstructured":"Toninho, B. , Caires, L. & Pfenning, F. (2011) Dependent session types via intuitionistic linear type theory. In Principles and Practice of Declarative Programming (PPDP).","DOI":"10.1145\/2003476.2003499"},{"key":"S0956796823000096_ref51","doi-asserted-by":"crossref","unstructured":"Strickland, T. S. , Tobin-Hochstadt, S. , Findler, R. B. & Flatt, M. (2012) Chaperones and impersonators: Run-time support for reasonable interposition. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA).","DOI":"10.1145\/2384616.2384685"},{"key":"S0956796823000096_ref36","doi-asserted-by":"crossref","unstructured":"Lazarek, L. , King, A. , Sundar, S. , Findler, R. B. & Dimoulas, C. (2020) Does blame shifting work? In Principles of Programming Languages (POPL).","DOI":"10.1145\/3371133"},{"key":"S0956796823000096_ref55","unstructured":"Swords, C. (2019) A Unified Characterization of Runtime Verification Systems as Patterns of Communication. Ph.D. thesis. Indiana University."},{"key":"S0956796823000096_ref53","doi-asserted-by":"crossref","unstructured":"Swaine, J. , Fetscher, B. , St-Amour, V. , Findler, R. B. & Flatt, M. (2012) Seeing the futures: Profiling shared-memory parallel racket. In Functional High-Performance Computing (FHPC).","DOI":"10.1145\/2364474.2364485"},{"key":"S0956796823000096_ref3","doi-asserted-by":"crossref","unstructured":"Ashley, J. M. & Dybvig, R. K. (1994) An efficient implementation of multiple return values in scheme. LISP and Funct. Program. (LFP).","DOI":"10.1145\/182409.156784"},{"key":"S0956796823000096_ref27","unstructured":"Gordon, C. S. (2017) A generic approach to flow-sensitive polymorphic effects. In European Conference on Object-Oriented Programming (ECOOP)."},{"key":"S0956796823000096_ref22","doi-asserted-by":"crossref","unstructured":"Findler, R. B. & Blume, M. (2006) Contracts as pairs of projections. In Functional and Logic Programming (FLP).","DOI":"10.1007\/11737414_16"},{"key":"S0956796823000096_ref4","doi-asserted-by":"crossref","unstructured":"Ballantyne, M. , King, A. & Felleisen, M. (2020) Macros for domain-specific languages. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA).","DOI":"10.1145\/3428297"},{"key":"S0956796823000096_ref5","unstructured":"Barendregt, H. P. (1981) The Lambda Calculus. North-Holland Publishing Co."},{"key":"S0956796823000096_ref10","doi-asserted-by":"crossref","unstructured":"Bocchi, L. , Honda, K. , Tuosto, E. & Yoshida, N. (2010) A theory of design-by-contract for distributed multiparty interactions. In International Conference on Concurrency Theory.","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"S0956796823000096_ref52","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","article-title":"Typestate: A programming language concept for enhancing software reliability","volume":"12","author":"Strom","year":"1986","journal-title":"IEEE Trans. Softw. Eng."},{"key":"S0956796823000096_ref19","doi-asserted-by":"crossref","unstructured":"Disney, T. , Flanagan, C. & McCarthy, J. (2011) Temporal higher-order contracts. In International Conference on Functional Programming (ICFP).","DOI":"10.1145\/2034773.2034800"},{"key":"S0956796823000096_ref12","doi-asserted-by":"crossref","unstructured":"Chen, F. & Ro\u015fu, G. (2007) MOP: An efficient and generic runtime verification framework. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA).","DOI":"10.1145\/1297027.1297069"},{"key":"S0956796823000096_ref25","unstructured":"Flatt, M. & PLT. (2010) Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design. Available at: https:\/\/racket-lang.org\/tr1\/."},{"key":"S0956796823000096_ref44","doi-asserted-by":"crossref","unstructured":"Nguy\u00ea\u0303n, P. C. , Gilray, T. , Tobin-Hochstadt, S. & Van Horn, D. (2018) Soft contract verification for higher-order stateful programs. In Principles of Programming Languages (POPL).","DOI":"10.1145\/3158139"},{"key":"S0956796823000096_ref31","doi-asserted-by":"crossref","unstructured":"Hinze, R. , Jeuring, J. & L\u00f6h, A. (2006) Typed contracts for functional programming. In Functional and Logic Programming (FLP).","DOI":"10.1007\/11737414_15"},{"key":"S0956796823000096_ref54","doi-asserted-by":"crossref","unstructured":"Swaine, J. , Tew, K. , Dinda, P. A. , Findler, R. B. & Flatt, M. (2010) Back to the futures: Incremental parallelization of existing sequential runtime systems. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA).","DOI":"10.1145\/1869459.1869507"},{"key":"S0956796823000096_ref30","doi-asserted-by":"crossref","unstructured":"Havelund, K. , Reger, G. , Thoma, D. & Z\u0103linescu, E. (2018) Monitoring events that carry data. In Lectures on Runtime Verification. Springer.","DOI":"10.1007\/978-3-319-75632-5_3"},{"key":"S0956796823000096_ref33","doi-asserted-by":"crossref","unstructured":"Jaspan, C. & Aldrich, J. (2009) Checking framework interactions with relationships. In European Conference on Object-Oriented Programming (ECOOP).","DOI":"10.21236\/ADA492512"},{"key":"S0956796823000096_ref47","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value and the \n\n\n\n$\\lambda$\n\n\n-calculus","volume":"1","author":"Plotkin","year":"1975","journal-title":"Theoretical Computer Science."},{"key":"S0956796823000096_ref61","doi-asserted-by":"crossref","unstructured":"Wolff, R. , Garcia, R. , Tanter, E. & Aldrich, J. (2011) Gradual typestate. In European Conference on Object-Oriented Programming (ECOOP).","DOI":"10.1007\/978-3-642-22655-7_22"},{"key":"S0956796823000096_ref43","doi-asserted-by":"crossref","unstructured":"Moy, C. , Nguy\u00ea\u0303n, P. C. , Tobin-Hochstadt, S. & Van Horn, D. (2021) Corpse reviver: Sound and efficient gradual typing via contract verification. In Principles of Programming Languages (POPL).","DOI":"10.1145\/3434334"},{"key":"S0956796823000096_ref13","unstructured":"Degen, M. , Thiemann, P. & Wehr, S. (2009) True lies: Lazy contracts for lazy languages (Faithfulness is better than laziness). In Arbeitstagung Programmiersprachen (ATPS)."},{"key":"S0956796823000096_ref24","doi-asserted-by":"crossref","unstructured":"Flatt, M. (2002) Composable and compilable macros: You want it when? In International Conference on Functional Programming (ICFP).","DOI":"10.1145\/581478.581486"},{"key":"S0956796823000096_ref28","doi-asserted-by":"crossref","unstructured":"Greenberg, M. , Pierce, B. C. & Weirich, S. (2010) Contracts made manifest. In Principles of Programming Languages (POPL).","DOI":"10.1145\/1706299.1706341"},{"key":"S0956796823000096_ref32","doi-asserted-by":"crossref","unstructured":"Honda, K. , Vasconcelos, V. T. & Kubo, M. (1998) Language primitives and type discipline for structured communication-based programming. In European Symposium on Programming (ESOP).","DOI":"10.1007\/BFb0053567"},{"key":"S0956796823000096_ref42","doi-asserted-by":"crossref","unstructured":"Moore, S. , Dimoulas, C. , Findler, R. B. , Flatt, M. & Chong, S. (2016) Extensible access control with authorization contracts. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA).","DOI":"10.1145\/2983990.2984021"},{"key":"S0956796823000096_ref6","doi-asserted-by":"crossref","unstructured":"Bartocci, E. , Falcone, Y. , Francalanza, A. & Reger, G. (2018) Introduction to runtime verification. In Lectures on Runtime Verification. Springer.","DOI":"10.1007\/978-3-319-75632-5"},{"key":"S0956796823000096_ref9","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796806005971","article-title":"Sound and complete models of contracts","volume":"16","author":"Blume","year":"2006","journal-title":"J. Funct. Program. (JFP)."},{"key":"S0956796823000096_ref50","volume-title":"Common Lisp the Language","author":"Steele","year":"1990"},{"key":"S0956796823000096_ref7","doi-asserted-by":"crossref","unstructured":"Beugnard, A. , J\u00e9z\u00e9quel, J.-M. & Plouzeau, N. (2010) Contract aware components, 10 years after. In International Workshop on Component and Service Interoperability (WCSI).","DOI":"10.4204\/EPTCS.37.1"},{"key":"S0956796823000096_ref41","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","article-title":"Applying \u201cdesign by contract\u201d","volume":"25","author":"Meyer","year":"1992","journal-title":"Computer."},{"key":"S0956796823000096_ref59","doi-asserted-by":"crossref","unstructured":"Tov, J. A. & Pucella, R. (2010) Stateful contracts for affine types. In European Symposium on Programming (ESOP).","DOI":"10.1007\/978-3-642-11957-6_29"},{"key":"S0956796823000096_ref16","doi-asserted-by":"crossref","unstructured":"Dimoulas, C. , Findler, R. B. , Flanagan, C. & Felleisen, M. (2011) Correct blame for contracts: No more scapegoating. In Principles of Programming Languages (POPL).","DOI":"10.1145\/1926385.1926410"},{"key":"S0956796823000096_ref56","doi-asserted-by":"crossref","unstructured":"Tate, R. (2013) The sequential semantics of producer effect systems. In Principles of Programming Languages (POPL).","DOI":"10.1145\/2429069.2429074"},{"key":"S0956796823000096_ref15","doi-asserted-by":"crossref","unstructured":"Dimoulas, C. , Findler, R. B. & Felleisen, M. (2013) Option contracts. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA).","DOI":"10.1145\/2509136.2509548"},{"key":"S0956796823000096_ref29","first-page":"1","article-title":"How to evaluate the performance of gradual typing systems","volume":"29","author":"Greenman","year":"2019","journal-title":"J. Funct. Program. (JFP)."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796823000096","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:37:01Z","timestamp":1779835021000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796823000096\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"references-count":62,"alternative-id":["S0956796823000096"],"URL":"https:\/\/doi.org\/10.1017\/s0956796823000096","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e14"}}