{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:56:10Z","timestamp":1776891370972,"version":"3.51.2"},"reference-count":44,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"1","license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2008,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higher-order abstract syntax. To fold over such a data type, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the data type are parametric. In this paper, we show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data structures containing functionals. From this implementation, we derive \u201cfusion laws\u201d that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Sch\u00fcrmann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System\n                    <jats:private-char>\n                      <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0956796807006557_char1\"\/>\n                    <\/jats:private-char>\n                    . This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.\n                  <\/jats:p>","DOI":"10.1017\/s0956796807006557","type":"journal-article","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T03:48:34Z","timestamp":1187754514000},"page":"87-140","source":"Crossref","is-referenced-by-count":25,"title":["Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism"],"prefix":"10.46298","volume":"18","author":[{"given":"GEOFFREY","family":"WASHBURN","sequence":"first","affiliation":[]},{"given":"STEPHANIE","family":"WEIRICH","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,1,1]]},"reference":[{"key":"S0956796807006557_manual_ref-28","volume-title":"Haskell 98 Language and Libraries: The Revised Report.","author":"Peyton Jones","year":"2003"},{"key":"S0956796807006557_manual_ref-14","volume-title":"Second Scandinavian Logic Symposium.","author":"Girard","year":"1971"},{"key":"S0956796807006557_manual_ref-20","volume-title":"Ninth European Symposium on Programming.","author":"Jones","year":"2000"},{"key":"S0956796807006557_manual_ref-42","volume-title":"Eighth ACM SIGPLAN International Conference on Functional Programming","author":"Washburn","year":"2003"},{"key":"S0956796807006557_manual_ref-3","volume-title":"Programming Languages and Their Definition.","author":"Beki\u0107","year":"1984"},{"key":"S0956796807006557_manual_ref-8","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/382780.382785","article-title":"A modal analysis of staged computation","volume":"48","author":"Davies","year":"2001","journal-title":"J. ACM"},{"key":"S0956796807006557_manual_ref-31","volume-title":"ACM SIGPLAN Conference on Programming Language Design and Implementation.","author":"Pfenning","year":"1988"},{"key":"S0956796807006557_manual_ref-6","volume-title":"The Generic Haskell User's Guide.","author":"Clarke","year":"2001"},{"key":"S0956796807006557_manual_ref-19","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001210"},{"key":"S0956796807006557_manual_ref-4","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"S0956796807006557_manual_ref-12","volume-title":"23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Fegaras","year":"1996"},{"key":"S0956796807006557_manual_ref-10","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1017\/S0960129501003346","article-title":"Recursion over objects of functional type","volume":"11","author":"Despeyroux","year":"2001","journal-title":"Math. Struct. Comput. Sci."},{"key":"S0956796807006557_manual_ref-33","volume-title":"Mathematics of Program Construction.","author":"Pitts","year":"2000"},{"key":"S0956796807006557_manual_ref-22","first-page":"967","article-title":"A theory on resolving equations in the space of languages","volume":"19","author":"Leszczy\u0142owski","year":"1971","journal-title":"Bull. Polish Acad. Sci."},{"key":"S0956796807006557_manual_ref-26","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1145\/1094622.1094628","article-title":"A proof theory for generic judgments","volume":"6","author":"Miller","year":"2005","journal-title":"ACM Trans. Computat. Logic."},{"key":"S0956796807006557_manual_ref-44","volume-title":"30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.","author":"Xi","year":"2003"},{"key":"S0956796807006557_manual_ref-23","volume-title":"Conference on Functional Programming Languages and Computer Architecture.","author":"Meijer","year":"1995"},{"key":"S0956796807006557_manual_ref-25","unstructured":"Miller, D. (1990, May) An extension to ML to handle bound variables in data structures: Preliminary report. Proceedings of the Logical Frameworks BRA Workshop."},{"key":"S0956796807006557_manual_ref-37","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_25"},{"key":"S0956796807006557_manual_ref-30","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"S0956796807006557_manual_ref-39","volume-title":"Fifth ACM SIGPLAN International Conference on Functional Programming.","author":"Trifonov","year":"2000"},{"key":"S0956796807006557_manual_ref-7","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001535"},{"key":"S0956796807006557_manual_ref-41","unstructured":"Washburn, G. (2001) Modal Typing for Specifying Run-time Code Generation. Available at http:\/\/www.cis.upenn.edu\/geoffw\/research\/. accessed 31 July 2007."},{"key":"S0956796807006557_manual_ref-16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_69"},{"key":"S0956796807006557_manual_ref-2","volume-title":"15th International Conference on Theorem Proving in Higher Order Logics.","author":"Ambler","year":"2002"},{"key":"S0956796807006557_manual_ref-11","volume-title":"Second International Conference on Typed Lambda Calculi and Applications.","author":"Despeyroux","year":"1995"},{"key":"S0956796807006557_manual_ref-27","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581498"},{"key":"S0956796807006557_manual_ref-21","doi-asserted-by":"publisher","DOI":"10.2307\/2964568"},{"key":"S0956796807006557_manual_ref-17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_78"},{"key":"S0956796807006557_manual_ref-24","volume-title":"Conference on Functional Programming Languages and Computer Architecture.","author":"Meijer","year":"1991"},{"key":"S0956796807006557_manual_ref-29","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"S0956796807006557_manual_ref-32","volume-title":"16th International Conference on Automated Deduction","author":"Pfenning","year":"1999"},{"key":"S0956796807006557_manual_ref-1","first-page":"14","volume-title":"30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Acar","year":"2002"},{"key":"S0956796807006557_manual_ref-35","unstructured":"Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism. Information Processing \/83. North-Holland. Proceedings of the IFIP 9th World Computer Congress."},{"key":"S0956796807006557_manual_ref-38","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012984529382"},{"key":"S0956796807006557_manual_ref-40","volume-title":"Conference on Functional Programming Languages and Computer Architecture.","author":"Wadler","year":"1989"},{"key":"S0956796807006557_manual_ref-13","doi-asserted-by":"crossref","unstructured":"Gabbay, M. J. & Cheney, J. (2004) A sequent calculus for nominal logic. In 19th IEEE Symposium on Logic in Computer Science.","DOI":"10.1109\/LICS.2004.1319608"},{"key":"S0956796807006557_manual_ref-34","unstructured":"Poswolsky, A. & Carsten Schrmann, C. (2007, Jan.). Delphin: A Functional Programming Language with Higher-Other Encodings and Dependent Types. Tech. Rept. YALEU\/DCS\/TR-1375. Yale University."},{"key":"S0956796807006557_manual_ref-36","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00418-7"},{"key":"S0956796807006557_manual_ref-9","volume-title":"IFIP International Theoretical Computer Science.","author":"Despeyroux","year":"2000"},{"key":"S0956796807006557_manual_ref-5","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0956796807006557_manual_ref-43","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005879"},{"key":"S0956796807006557_manual_ref-18","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022982420888"},{"key":"S0956796807006557_manual_ref-15","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0167-6423(02)00025-4","article-title":"Polytypic values possess polykinded types","volume":"43","author":"Hinze","year":"2002","journal-title":"Sci. Computer Programming"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006557","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:12Z","timestamp":1776889152000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006557\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["S0956796807006557"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006557","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1]]}}}