{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:29:39Z","timestamp":1725892179357},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313646"},{"type":"electronic","value":"9783642313653"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31365-3_36","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T16:35:34Z","timestamp":1340296534000},"page":"462-476","source":"Crossref","is-referenced-by-count":5,"title":["Correctness of Program Transformations as a Termination Problem"],"prefix":"10.1007","author":[{"given":"Conrad","family":"Rau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Sabel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"36_CR1","series-title":"Its Syntax and Semantics","volume-title":"The Lambda Calculus","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam (1984)"},{"key":"36_CR2","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schau\u00df, M. (ed.) RTA 22. LIPIcs, vol.\u00a010, pp. 21\u201330. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"issue":"3","key":"36_CR3","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1025689206562","volume":"16","author":"J. Ford","year":"2003","unstructured":"Ford, J., Mason, I.A.: Formal foundations of operational semantics. Higher Order Symbol. Comput.\u00a016(3), 161\u2013202 (2003)","journal-title":"Higher Order Symbol. Comput."},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02348-4_3","volume-title":"Rewriting Techniques and Applications","author":"C. Fuhs","year":"2009","unstructured":"Fuhs, C., Giesl, J., Pl\u00fccker, M., Schneider-Kamp, P., Falke, S.: Proving Termination of Integer Term Rewriting. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 32\u201347. Springer, Heidelberg (2009)"},{"key":"36_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"36_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-02348-4_21","volume-title":"Rewriting Techniques and Applications","author":"M. Korp","year":"2009","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 295\u2013304. Springer, Heidelberg (2009)"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Kutzner, A., Schmidt-Schau\u00df, M.: A nondeterministic call-by-need lambda calculus. In: Felleisen, M., Hudak, P., Queinnec, C. (eds.) 3rd ICFP, pp. 324\u2013335. ACM (1998)","DOI":"10.1145\/291251.289462"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-46425-5_17","volume-title":"Programming Languages and Systems","author":"E. Machkasova","year":"2000","unstructured":"Machkasova, E., Turbak, F.A.: A Calculus for Link-Time Compilation. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, pp. 260\u2013274. Springer, Heidelberg (2000)"},{"issue":"1","key":"36_CR9","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/j.entcs.2004.09.041","volume":"128","author":"M. Mann","year":"2005","unstructured":"Mann, M.: Congruence of bisimulation in a non-deterministic call-by-need lambda calculus. Electron. Notes Theor. Comput. Sci.\u00a0128(1), 81\u2013101 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"36_CR10","unstructured":"Morris, J.H.: Lambda-Calculus Models of Programming Languages. PhD thesis. MIT (1968)"},{"key":"36_CR11","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1016\/j.entcs.2007.02.041","volume":"173","author":"J. Niehren","year":"2007","unstructured":"Niehren, J., Sabel, D., Schmidt-Schau\u00df, M., Schwinghammer, J.: Observational semantics for a concurrent lambda calculus with reference cells and futures. Electron. Notes Theor. Comput. Sci.\u00a0173, 313\u2013337 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"36_CR12","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1016\/j.tcs.2006.08.016","volume":"364","author":"J. Niehren","year":"2006","unstructured":"Niehren, J., Schwinghammer, J., Smolka, G.: A concurrent lambda calculus with futures. Theoret. Comput. Sci.\u00a0364(3), 338\u2013356 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"36_CR13","unstructured":"Peyton Jones, S.: Haskell 98 language and libraries: the Revised Report. Cambridge University Press (2003)"},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"Peyton Jones, S., Gordon, A., Finne, S.: Concurrent Haskell. In: Steele, G. (ed.) 23th POPL, pp. 295\u2013308. ACM (1996)","DOI":"10.1145\/237721.237794"},{"key":"36_CR15","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G.D. Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value, and the lambda-calculus. Theoret. Comput. Sci.\u00a01, 125\u2013159 (1975)","journal-title":"Theoret. Comput. Sci."},{"key":"36_CR16","doi-asserted-by":"crossref","unstructured":"Rau, C., Schmidt-Schau\u00df, M.: Towards correctness of program transformations through unification and critical pair computation. In: Fernandez, M. (ed.) 24th UNIF. EPTCS, vol.\u00a042, pp. 39\u201354 (2010)","DOI":"10.4204\/EPTCS.42.4"},{"key":"36_CR17","unstructured":"Rau, C., Schmidt-Schau\u00df, M.: A unification algorithm to compute overlaps in a call-by-need lambda-calculus with variable-binding chains. In: Baader, F., Morawska, B., Otop, J. (eds.) 25th UNIF, pp. 35\u201341 (2011)"},{"issue":"03","key":"36_CR18","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1017\/S0960129508006774","volume":"18","author":"D. Sabel","year":"2008","unstructured":"Sabel, D., Schmidt-Schau\u00df, M.: A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci.\u00a018(03), 501\u2013553 (2008)","journal-title":"Math. Structures Comput. Sci."},{"key":"36_CR19","doi-asserted-by":"crossref","unstructured":"Sabel, D., Schmidt-Schau\u00df, M.: A contextual semantics for Concurrent Haskell with futures. In: Hanus, M. (ed.) 13th PPDP, pp. 101\u2013112. ACM (2011)","DOI":"10.1145\/2003476.2003492"},{"issue":"11-13","key":"36_CR20","doi-asserted-by":"publisher","first-page":"1521","DOI":"10.1016\/j.tcs.2009.12.001","volume":"411","author":"M. Schmidt-Schau\u00df","year":"2010","unstructured":"Schmidt-Schau\u00df, M., Sabel, D.: On generic context lemmas for higher-order calculi with sharing. Theoret. Comput. Sci.\u00a0411(11-13), 1521\u20131541 (2010)","journal-title":"Theoret. Comput. Sci."},{"issue":"04","key":"36_CR21","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1017\/S0956796807006624","volume":"18","author":"M. Schmidt-Schau\u00df","year":"2008","unstructured":"Schmidt-Schau\u00df, M., Sch\u00fctz, M., Sabel, D.: Safety of N\u00f6cker\u2019s strictness analysis. J. Funct. Programming\u00a018(04), 503\u2013551 (2008)","journal-title":"J. Funct. Programming"},{"key":"36_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/3-540-44881-0_8","volume-title":"Rewriting Techniques and Applications","author":"J.B. Wells","year":"2003","unstructured":"Wells, J.B., Plump, D., Kamareddine, F.: Diagrams for Meaning Preservation. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 88\u2013106. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31365-3_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:58:28Z","timestamp":1620115108000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31365-3_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313646","9783642313653"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31365-3_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}