{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T15:54:54Z","timestamp":1756310094949},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,9,1]],"date-time":"2009-09-01T00:00:00Z","timestamp":1251763200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2009,9]]},"DOI":"10.1007\/s10990-010-9050-z","type":"journal-article","created":{"date-parts":[[2010,1,18]],"date-time":"2010-01-18T15:16:10Z","timestamp":1263827770000},"page":"199-231","source":"Crossref","is-referenced-by-count":5,"title":["A verified framework for higher-order uncurrying optimizations"],"prefix":"10.1007","volume":"22","author":[{"given":"Zaynah","family":"Dargaye","sequence":"first","affiliation":[]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,1,19]]},"reference":[{"issue":"4","key":"9050_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.L., L\u00e9vy, J.J.: Explicit substitutions. J. Funct. Program. 1(4), 375\u2013416 (1991)","journal-title":"J. Funct. Program."},{"key":"9050_CR2","first-page":"309","volume-title":"35th Symposium Principles of Programming Languages","author":"U.A. Acar","year":"2008","unstructured":"Acar, U.A., Ahmed, A., Blume, M.: Imperative self-adjusting computation. In: 35th Symposium Principles of Programming Languages, pp. 309\u2013322. ACM, New York (2008)"},{"key":"9050_CR3","series-title":"Studies in Logics and the Foundations of Mathematics","first-page":"739","volume-title":"Handbook of Mathematical Logic","author":"P. Aczel","year":"1997","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic. Studies in Logics and the Foundations of Mathematics, vol. 90, pp. 739\u2013782. North-Holland, Amsterdam (1997)"},{"key":"9050_CR4","unstructured":"Ahmed, A.J.: Semantics of types for mutable state. Ph.D. thesis,. Princeton University (2004)"},{"key":"9050_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/11693024_6","volume-title":"Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006","author":"A.J. Ahmed","year":"2006","unstructured":"Ahmed, A.J.: Step-indexed syntactic logical relations for recursive and quantified types. In: Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006. Lecture Notes in Computer Science, vol. 3924, pp. 69\u201383. Springer, Berlin (2006)"},{"key":"9050_CR6","first-page":"247","volume-title":"Logic in Computer Science 2001","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Logic in Computer Science 2001, pp. 247\u2013258. IEEE Computer Society, Los Alamitos (2001)"},{"issue":"5","key":"9050_CR7","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657\u2013683 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9050_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Int. Conf. on Theorem Proving in Higher Order Logics (TPHOLs)","author":"B.E. Aydemir","year":"2005","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: the POPLmark challenge. In: Int. Conf. on Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science, vol. 3603, pp. 50\u201365. Springer, Berlin (2005)"},{"key":"9050_CR9","series-title":"EATCS Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, Berlin (2004)"},{"key":"9050_CR10","series-title":"Handbook of the History of Logic","volume-title":"Logic from Russell to Church","author":"F. Cardone","year":"2009","unstructured":"Cardone, F., Hindley, J.R.: History of lambda-calculus and combinatory logic. In: Gabbay, D.M., Woods,\u00a0J. (eds.) Logic from Russell to Church. Handbook of the History of Logic, vol. 5. North-Holland, Amsterdam (2009)"},{"key":"9050_CR11","unstructured":"Coq development team: The Coq proof assistant. Software and documentation available at http:\/\/coq.inria.fr\/ (1989\u20132009)"},{"issue":"2","key":"9050_CR12","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0167-6423(87)90020-7","volume":"8","author":"G. Cousineau","year":"1987","unstructured":"Cousineau, G., Curien, P.L., Mauny, M.: The categorical abstract machine. Sci. Comput. Program. 8(2), 173\u2013202 (1987)","journal-title":"Sci. Comput. Program."},{"key":"9050_CR13","volume-title":"Combinatory Logic","author":"H.B. Curry","year":"1958","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic, vol.\u00a0I. North-Holland, Amsterdam (1958). 3rd edn. 1974"},{"key":"9050_CR14","first-page":"119","volume-title":"Journ\u00e9es Francophones des Langages Applicatifs (JFLA\u201907","author":"Z. Dargaye","year":"2007","unstructured":"Dargaye, Z.: D\u00e9curryfication certifi\u00e9e. In: Journ\u00e9es Francophones des Langages Applicatifs (JFLA\u201907, pp. 119\u2013134. INRIA, Rocquencourt (2007)"},{"key":"9050_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2572-0","volume-title":"Isomorphisms of Types: From Lambda Calculus to Information Retrieval and Language Design","author":"R. Cosmo Di","year":"1995","unstructured":"Di Cosmo, R.: Isomorphisms of Types: From Lambda Calculus to Information Retrieval and Language Design. Birkhauser, Basel (1995)"},{"key":"9050_CR16","first-page":"131","volume-title":"Formal Description of Programming Concepts\u00a0III","author":"M. Felleisen","year":"1986","unstructured":"Felleisen, M., Friedman, D.P.: Control operators, the SECD machine and the \u03bb-calculus. In: Formal Description of Programming Concepts\u00a0III, pp. 131\u2013141. North-Holland, Amsterdam (1986)"},{"key":"9050_CR17","first-page":"245","volume-title":"33rd Symposium Principles of Programming Languages","author":"C. Flanagan","year":"2006","unstructured":"Flanagan, C.: Hybrid type checking. In: 33rd Symposium Principles of Programming Languages, pp. 245\u2013256. ACM, New York (2006)"},{"key":"9050_CR18","first-page":"27","volume-title":"International Conference on Functional Programming 1998","author":"J. Hannan","year":"1998","unstructured":"Hannan, J., Hicks, P.: Higher-order arity raising. In: International Conference on Functional Programming 1998, pp. 27\u201338. ACM, New York (1998)"},{"issue":"3","key":"9050_CR19","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1023\/A:1010006229549","volume":"13","author":"J. Hannan","year":"2000","unstructured":"Hannan, J., Hicks, P.: Higher-order uncurrying. High.-Order Symb. Comput. 13(3), 179\u2013216 (2000)","journal-title":"High.-Order Symb. Comput."},{"issue":"3","key":"9050_CR20","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0167-6423(94)00004-2","volume":"22","author":"F. Henglein","year":"1994","unstructured":"Henglein, F.: Dynamic typing: syntax and proof theory. Sci. Comput. Program. 22(3), 197\u2013230 (1994)","journal-title":"Sci. Comput. Program."},{"key":"9050_CR21","first-page":"213","volume-title":"21st Symposium Principles of Programming Languages","author":"F. Henglein","year":"1994","unstructured":"Henglein, F., J\u00f8rgensen, J.: Formally optimal boxing. In: 21st Symposium Principles of Programming Languages, pp. 213\u2013226. ACM, New York (1994)"},{"issue":"3","key":"9050_CR22","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/s10990-007-9018-9","volume":"20","author":"J.L. Krivine","year":"2007","unstructured":"Krivine, J.L.: A call-by-name lambda-calculus machine. High.-Order Symb. Comput. 20(3), 199\u2013207 (2007)","journal-title":"High.-Order Symb. Comput."},{"key":"9050_CR23","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P.J. Landin","year":"1964","unstructured":"Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6, 308\u2013320 (1964)","journal-title":"Comput. J."},{"key":"9050_CR24","unstructured":"Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA (1990)"},{"key":"9050_CR25","first-page":"177","volume-title":"19th Symposium Principles of Programming Languages","author":"X. Leroy","year":"1992","unstructured":"Leroy, X.: Unboxed objects and polymorphic typing. In: 19th Symposium Principles of Programming Languages, pp. 177\u2013188. ACM, New York (1992)"},{"key":"9050_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008","author":"P. Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: An overview. In: Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008. Lecture Notes in Computer Science, vol.\u00a05028, pp. 359\u2013369. Springer, Berlin (2008)"},{"issue":"4\u20135","key":"9050_CR27","first-page":"375","volume":"16","author":"S. Marlow","year":"2006","unstructured":"Marlow, S., Peyton Jones, S.: Making a fast curry: push\/enter vs eval\/apply for higher-order languages. J. Funct. Program. 16(4\u20135), 375\u2013414 (2006)","journal-title":"J. Funct. Program."},{"key":"9050_CR28","first-page":"106","volume-title":"24th Symposium Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: 24th Symposium Principles of Programming Languages, pp. 106\u2013119. ACM, New York (1997)"},{"key":"9050_CR29","first-page":"83","volume-title":"Programming Language Design and Implementation 2000","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation 2000, pp. 83\u201395. ACM, New York (2000)"},{"issue":"2","key":"9050_CR30","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1017\/S0956796800000319","volume":"2","author":"S.L. Peyton Jones","year":"1992","unstructured":"Peyton Jones, S.L.: Implementing lazy functional languages on stock hardware: the spineless tagless G-machine. J. Funct. Program. 2(2), 127\u2013202 (1992)","journal-title":"J. Funct. Program."},{"key":"9050_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, TACAS \u201998","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Tools and Algorithms for Construction and Analysis of Systems, TACAS \u201998. Lecture Notes in Computer Science, vol. 1384, pp. 151\u2013166. Springer, Berlin (1998)"},{"key":"9050_CR32","first-page":"164","volume-title":"Programming Language Design and Implementation 1988","author":"O. Shivers","year":"1988","unstructured":"Shivers, O.: Control-flow analysis in Scheme. In: Programming Language Design and Implementation 1988, pp. 164\u2013174. ACM, New York (1988)"},{"key":"9050_CR33","unstructured":"Siek, J.G., Taha, W.: Gradual typing for functional languages. In: Scheme and Functional Programming 2006, pp. 81\u201392. Technical report TR-2006-06, University of Chicago (2006)"},{"issue":"2\/3","key":"9050_CR34","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"Statman, R.: Logical relations and the typed \u03bb-calculus. Inf. Control 65(2\/3), 85\u201397 (1985)","journal-title":"Inf. Control"},{"key":"9050_CR35","first-page":"367","volume-title":"17th Symposium Principles of Programming Languages","author":"S.R. Thatte","year":"1990","unstructured":"Thatte, S.R.: Quasi-static typing. In: 17th Symposium Principles of Programming Languages, pp. 367\u2013381. ACM, New York (1990)"},{"key":"9050_CR36","first-page":"17","volume-title":"35th Symposium Principles of Programming Languages","author":"J.B. Tristan","year":"2008","unstructured":"Tristan, J.B., Leroy, X.: Formal verification of translation validators: a case study on instruction scheduling optimizations. In: 35th Symposium Principles of Programming Languages, pp. 17\u201327. ACM, New York (2008)"},{"issue":"3","key":"9050_CR37","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1017\/S0956796801004245","volume":"12","author":"J.B. Wells","year":"2002","unstructured":"Wells, J.B., Dimock, A., Muller, R., Turbak, F.: A calculus for polymorphic and polyvariant flow types. J. Funct. Program. 12(3), 183\u2013227 (2002)","journal-title":"J. Funct. Program."},{"issue":"1","key":"9050_CR38","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/239912.239917","volume":"19","author":"A.K. Wright","year":"1997","unstructured":"Wright, A.K., Cartwright, R.: A practical soft type system for scheme. ACM Trans. Program. Lang. Syst. 19(1), 87\u2013152 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-010-9050-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-010-9050-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-010-9050-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T01:29:41Z","timestamp":1559352581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-010-9050-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,9]]}},"alternative-id":["9050"],"URL":"https:\/\/doi.org\/10.1007\/s10990-010-9050-z","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9]]}}}