{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:05:56Z","timestamp":1765667156143,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662494974"},{"type":"electronic","value":"9783662494981"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_29","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T13:36:06Z","timestamp":1458567366000},"page":"752-779","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs"],"prefix":"10.1007","author":[{"given":"Yuting","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gopalan","family":"Nadathur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11693024_6","volume-title":"Programming Languages and Systems","author":"A Ahmed","year":"2006","unstructured":"Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 69\u201383. Springer, Heidelberg (2006)"},{"issue":"5","key":"29_CR2","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"AW Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.: 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":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"BE Aydemir","year":"2005","unstructured":"Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"issue":"2","key":"29_CR4","first-page":"1","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formalized Reasoning 7(2), 1\u201389 (2014)","journal-title":"J. Formalized Reasoning"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Baelde, D., Nadathur, G.: Combining deduction modulo and logics of fixed-point definitions. In: Proceedings of the 2012 27th Annual IEEE\/ACM Symposium on Logic in Computer Science, pp. 105\u2013114. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.22"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"B\u00e9langer, O.S., Chaudhuri, K.: Automatically deriving schematic theorems for dynamic contexts. In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. ACM Press (2014)","DOI":"10.1145\/2631172.2631181"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-03545-1_16","volume-title":"Certified Programs and Proofs","author":"O Savary-Belanger","year":"2013","unstructured":"Savary-Belanger, O., Monnier, S., Pientka, B.: Programming type-safe transformations using higher-order abstract syntax. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 243\u2013258. Springer, Heidelberg (2013)"},{"key":"29_CR8","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"issue":"5","key":"29_CR9","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"NG Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indagationes Mathematicae 34(5), 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"29_CR10","doi-asserted-by":"crossref","first-page":"33","DOI":"10.4204\/EPTCS.185.3","volume":"185","author":"Andrew Cave","year":"2015","unstructured":"Cave, A., Pientka, B.: A case study on logical relations using contextual types. In: Proceedings of the Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, EPTCS, vol. 185, pp. 33\u201345 (2015)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 54\u201365. ACM Press (2007)","DOI":"10.1145\/1250734.1250742"},{"key":"29_CR12","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"key":"29_CR13","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500001535","volume":"2","author":"O Danvy","year":"1992","unstructured":"Danvy, O., Filinski, A.: Representing control: a study of the CPS transformation. Math. Struct. Comput. Sci. 2, 361\u2013391 (1992)","journal-title":"Math. Struct. Comput. Sci."},{"key":"29_CR14","unstructured":"Dargaye, Z.: V\u00e9rification formelle d\u2019un compilateur optimisant pour langages fonctionnels. Ph.D. thesis, l\u2019Universit\u00e9 Paris 7-Denis Diderot, France (2009)"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C.: Introduction to the HOL system. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, pp. 2\u20133. IEEE Computer Society (1991)","DOI":"10.1109\/HOL.1991.596265"},{"key":"29_CR16","unstructured":"Hannan, J., Pfenning, F.: Compiler verification in LF. In: 7th Symposium on Logic in Computer Science. IEEE Computer Society Press (1992)"},{"issue":"1","key":"29_CR17","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"issue":"2\u20133","key":"29_CR18","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/s10990-006-8746-6","volume":"19","author":"J Hickey","year":"2006","unstructured":"Hickey, J., Nogin, A.: Formal compiler construction in a logical framework. Higher-Order Symb. Comput. 19(2\u20133), 197\u2013230 (2006)","journal-title":"Higher-Order Symb. Comput."},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Hur, C.K., Dreyer, D.: A Kripke logical relation between ML and assembly. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 133\u2013146. ACM Press (2011)","DOI":"10.1145\/1926385.1926402"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179\u2013191. ACM Press (2014)","DOI":"10.1145\/2535838.2535841"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 42\u201354. ACM Press (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. In: Proceedings of Symposia in Applied Mathematics. Mathematical Aspects of Computer Science, vol. 19, pp. 33\u201341. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"29_CR23","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoret. Comput. Sci. 232, 91\u2013119 (2000)","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/3-540-44957-4_16","volume-title":"Computational Logic - CL 2000","author":"D Miller","year":"2000","unstructured":"Miller, D.: Abstract syntax for variable binders: an overview. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 239\u2013253. Springer, Heidelberg (2000)"},{"key":"29_CR25","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order Logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)"},{"issue":"4","key":"29_CR26","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Logic 6(4), 749\u2013783 (2005)","journal-title":"ACM Trans. Comput. Logic"},{"key":"29_CR27","first-page":"51","volume-title":"Machine Intelligence","author":"R Milner","year":"1972","unstructured":"Milner, R., Weyrauch, R.: Proving compiler correctness in a mechanized logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 51\u201372. Edinburgh University Press, Edinburgh (1972)"},{"key":"29_CR28","unstructured":"Minamide, Y., Morrisett, G., Harper, R.: Typed closure conversion. Technical report CMU-CS-95-171, School of Computer Science, Carnegie Mellon University (1995)"},{"key":"29_CR29","unstructured":"Murphy VII, T.: Modal types for mobile code. Ph.D. thesis, Carnegie Mellon University (2008)"},{"key":"29_CR30","unstructured":"Nadathur, G., Miller, D.: An overview of $$\\lambda $$ \u03bb Prolog. In: Fifth International Logic Programming Conference, pp. 810\u2013827. MIT Press (1988)"},{"issue":"3","key":"29_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1352582.1352591","volume":"9","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual model type theory. ACM Trans. Comput. Logic 9(3), 1\u201349 (2008)","journal-title":"ACM Trans. Comput. Logic"},{"key":"29_CR32","doi-asserted-by":"crossref","unstructured":"Neis, G., Hur, C.K., Kaiser, J.O., McLaughlin, C., Dreyer, D., Vafeiadis, V.: Pilsner: a compositionally verified compiler for a higher-order imperative language. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp. 166\u2013178. ACM Press (2015)","DOI":"10.1145\/2858949.2784764"},{"key":"29_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"29_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-14203-1_2","volume-title":"Automated Reasoning","author":"B Pientka","year":"2010","unstructured":"Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 15\u201321. Springer, Heidelberg (2010)"},{"issue":"2","key":"29_CR35","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"AM Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"key":"29_CR36","unstructured":"Qi, X., Gacek, A., Holte, S., Nadathur, G., Snow, Z.: The Teyjus system - Version 2. http:\/\/teyjus.cs.umn.edu\/"},{"key":"29_CR37","unstructured":"Tian, Y.H.: Mechanically verifying correctness of CPS compilation. In: Twelfth Computing: The Australasian Theory Symposium. CRPIT, vol. 51, pp. 41\u201351. ACS (2006)"},{"key":"29_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-642-31365-3_43","volume-title":"Automated Reasoning","author":"A Tiu","year":"2012","unstructured":"Tiu, A.: Stratification in logics of definitions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 544\u2013558. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:35:26Z","timestamp":1748813726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}