{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:13:02Z","timestamp":1774987982692,"version":"3.50.1"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2012,5,29]],"date-time":"2012-05-29T00:00:00Z","timestamp":1338249600000},"content-version":"unspecified","delay-in-days":28,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2012,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Since Findler and Felleisen (Findler, R. B. &amp; Felleisen, M. 2002) introduced<jats:italic>higher-order contracts<\/jats:italic>, many variants have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen (2002) in using<jats:italic>latent<\/jats:italic>contracts, purely dynamic checks that are transparent to the type system; others use<jats:italic>manifest<\/jats:italic>contracts, where<jats:italic>refinement types<\/jats:italic>record the most recent check that has been applied to each value. These two approaches are commonly assumed to be equivalent\u2014different ways of implementing the same idea, one retaining a simple type system, and the other providing more static information. Our goal is to formalize and clarify this folklore understanding. Our work extends that of Gronski and Flanagan (Gronski, J. &amp; Flanagan, C. 2007), who defined a latent calculus \u03bb<jats:sub>C<\/jats:sub>and a manifest calculus \u03bb<jats:sub>H<\/jats:sub>, gave a translation \u03c6 from \u03bb<jats:sub>C<\/jats:sub>to \u03bb<jats:sub>H<\/jats:sub>, and proved that if a \u03bb<jats:sub>C<\/jats:sub>term reduces to a constant, so does its \u03c6-image. We enrich their account with a translation \u03c8 from \u03bb<jats:sub>H<\/jats:sub>to \u03bb<jats:sub>C<\/jats:sub>and prove an analogous theorem. We then generalize the whole framework to<jats:italic>dependent contracts<\/jats:italic>, whose predicates can mention free variables. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of \u03bb<jats:sub>H<\/jats:sub>and two dialects (\u201clax\u201d and \u201cpicky\u201d) of \u03bb<jats:sub>C<\/jats:sub>, establish type soundness\u2014a substantial result in itself, for \u03bb<jats:sub>H<\/jats:sub>\u2014 and extend \u03c6 and \u03c8 accordingly. Surprisingly, the intuition that the latent and manifest systems are equivalent now breaks down: the extended translations preserve behavior in one direction, but in the other, sometimes yield terms that blame more.<\/jats:p>","DOI":"10.1017\/s0956796812000135","type":"journal-article","created":{"date-parts":[[2012,5,29]],"date-time":"2012-05-29T12:49:56Z","timestamp":1338295796000},"page":"225-274","source":"Crossref","is-referenced-by-count":8,"title":["Contracts made manifest"],"prefix":"10.1017","volume":"22","author":[{"given":"MICHAEL","family":"GREENBERG","sequence":"first","affiliation":[]},{"given":"BENJAMIN C.","family":"PIERCE","sequence":"additional","affiliation":[]},{"given":"STEPHANIE","family":"WEIRICH","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2012,5,29]]},"reference":[{"key":"S0956796812000135_ref9","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1145\/581478.581484","volume-title":"Proceedings of the Seventh ACM SIGPLAN International Conference on International Conference on Functional Programming (ICFP)","author":"Findler","year":"2002"},{"key":"S0956796812000135_ref5","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"S0956796812000135_ref21","first-page":"395","volume-title":"Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Tobin-Hochstadt","year":"2008"},{"key":"S0956796812000135_ref12","first-page":"54","volume-title":"Proceedings of the 8th Symposium on Trends in Functional Programming (TFP)","author":"Gronski","year":"2007"},{"key":"S0956796812000135_ref3","first-page":"18","volume-title":"Proceedings of the European Symposium on Programming (ESOP)","author":"Belo","year":"2011"},{"key":"S0956796812000135_ref25","first-page":"41","volume-title":"Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages (POPL)","author":"Xu","year":"2009"},{"key":"S0956796812000135_ref11","first-page":"353","volume-title":"Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on the Principles of Programming Languages (POPL)","author":"Greenberg","year":"2010"},{"key":"S0956796812000135_ref7","first-page":"215","volume-title":"Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Dimoulas","year":"2011"},{"key":"S0956796812000135_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_16"},{"key":"S0956796812000135_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005971"},{"key":"S0956796812000135_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"S0956796812000135_ref16","first-page":"93","volume-title":"Proceedings of the Scheme and Functional Programming Workshop","author":"Knowles","year":"2006"},{"key":"S0956796812000135_ref2","volume-title":"LNgen: Tool support for locally nameless representations","author":"Aydemir","year":"2010"},{"key":"S0956796812000135_ref23","first-page":"1","volume-title":"Proceedings of the 18th European Symposium on Programming (ESOP)","author":"Wadler","year":"2009"},{"key":"S0956796812000135_ref19","first-page":"245","volume-title":"Advanced Topics in Types and Programming Languages, Chap. 7","author":"Pitts","year":"2005"},{"key":"S0956796812000135_ref24","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796812000135_ref20","first-page":"1","volume-title":"Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Sewell","year":"2007"},{"key":"S0956796812000135_ref10","first-page":"245","volume-title":"Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages (POPL)","author":"Flanagan","year":"2006"},{"key":"S0956796812000135_ref13","first-page":"29","volume-title":"Proceedings of the Dynamic Languages Symposium (DLS)","author":"Guha","year":"2007"},{"key":"S0956796812000135_ref17","volume-title":"Eiffel: The Language","author":"Meyer","year":"1992"},{"key":"S0956796812000135_ref1","first-page":"69","volume-title":"Proceedings of the European Symposium on Programming (ESOP)","author":"Ahmed","year":"2006"},{"key":"S0956796812000135_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_15"},{"key":"S0956796812000135_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_4"},{"key":"S0956796812000135_ref22","volume-title":"Proceedings of the Scheme and Functional Programming Workshop","author":"Wadler","year":"2007"},{"key":"S0956796812000135_ref18","first-page":"437","volume-title":"Proceedings of the IFIP Conference on Theoretical Computer Science (TCS)","author":"Ou","year":"2004"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796812000135","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,16]],"date-time":"2022-01-16T12:14:04Z","timestamp":1642335244000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796812000135\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,5]]}},"alternative-id":["S0956796812000135"],"URL":"https:\/\/doi.org\/10.1017\/s0956796812000135","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5]]}}}