{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:52:14Z","timestamp":1762458734239,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642034282"},{"type":"electronic","value":"9783642034299"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03429-9_10","type":"book-chapter","created":{"date-parts":[[2009,8,28]],"date-time":"2009-08-28T12:12:52Z","timestamp":1251461572000},"page":"135-151","source":"Crossref","is-referenced-by-count":7,"title":["A Rewriting Logic Approach to Type Inference"],"prefix":"10.1007","author":[{"given":"Chucky","family":"Ellison","sequence":"first","affiliation":[]},{"given":"Traian Florin","family":"\u015eerb\u0103nu\u0163\u0103","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-25984-8_1","volume-title":"Automated Reasoning","author":"J. Meseguer","year":"2004","unstructured":"Meseguer, J., Ro\u015fu, G.: Rewriting logic semantics: From language specifications to formal analysis tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol.\u00a03097, pp. 1\u201344. Springer, Heidelberg (2004)"},{"issue":"3","key":"10_CR2","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.tcs.2006.12.018","volume":"373","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Ro\u015fu, G.: The rewriting logic semantics project. J. TCS\u00a0373(3), 213\u2013237 (2007)","journal-title":"J. TCS"},{"key":"10_CR3","unstructured":"Ro\u015fu, G.: K: A rewrite-based framework for modular language design, semantics, analysis and implementation. Technical Report UIUCDCS-R-2006-2802, Computer Science Department, University of Illinois at Urbana-Champaign (2006)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-540-71316-6_29","volume-title":"Programming Languages and Systems","author":"G. Kuan","year":"2007","unstructured":"Kuan, G., MacQueen, D., Findler, R.B.: A rewriting semantics for type inference. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 426\u2013440. Springer, Heidelberg (2007)"},{"issue":"2","key":"10_CR5","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M. Felleisen","year":"1992","unstructured":"Felleisen, M., Hieb, R.: A revised report on the syntactic theories of sequential control and state. J. TCS\u00a0103(2), 235\u2013271 (1992)","journal-title":"J. TCS"},{"issue":"1","key":"10_CR6","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115(1), 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-540-25979-4_21","volume-title":"Rewriting Techniques and Applications","author":"J. Matthews","year":"2004","unstructured":"Matthews, J., Findler, R.B., Flatt, M., Felleisen, M.: A visual environment for developing context-sensitive term rewriting systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 301\u2013311. Springer, Heidelberg (2004)"},{"issue":"3","key":"10_CR8","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Computer and System Sciences\u00a017(3), 348\u2013375 (1978)","journal-title":"J. Computer and System Sciences"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Bravenboer, M., Kalleberg, K.T., Vermaas, R., Visser, E.: Stratego\/XT Tutorial, Examples, and Reference Manual. Department of Information and Computing Sciences, Universiteit Utrecht (August 2005) (Draft)","DOI":"10.1145\/1111542.1111558"},{"issue":"2","key":"10_CR10","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"Barendregt, H.: Introduction to generalized type systems. J. Functional Programming\u00a01(2), 125\u2013154 (1991)","journal-title":"J. Functional Programming"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-39993-3_16","volume-title":"From Object-Orientation to Formal Methods","author":"M.-O. Stehr","year":"2004","unstructured":"Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol.\u00a02635, pp. 334\u2013375. Springer, Heidelberg (2004)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-17945-3_8","volume-title":"PARLE Parallel Architectures and Languages Europe","author":"H.P. Barendregt","year":"1987","unstructured":"Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, R., Plasmeijer, M.J., Sleep, M.R.: Term graph rewriting. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE 1987. LNCS, vol.\u00a0259, pp. 141\u2013158. Springer, Heidelberg (1987)"},{"key":"10_CR13","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation","author":"D. Plump","year":"1998","unstructured":"Plump, D.: Term graph rewriting. In: Handbook of Graph Grammars and Computing by Graph Transformation, vol.\u00a02. World Scientific, Singapore (1998)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/3-540-56393-8_4","volume-title":"Conditional Term Rewriting Systems","author":"R. Banach","year":"1993","unstructured":"Banach, R.: Simple type inference for term graph rewriting systems. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 51\u201366. Springer, Heidelberg (1993)"},{"key":"10_CR15","first-page":"112","volume-title":"PEPM 2007","author":"S. Fogarty","year":"2007","unstructured":"Fogarty, S., Pasalic, E., Siek, J., Taha, W.: Concoqtion: Indexed types now! In: PEPM 2007, pp. 112\u2013121. ACM, New York (2007)"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Kamareddine, F., Klop, J.W.(eds.): Special Issue on Type Theory and Term Rewriting: A Collection of Papers. Journal of Logic and Computation\u00a0 10(3). Oxford University Press, Oxford (2000)","DOI":"10.1093\/logcom\/10.3.321"},{"key":"10_CR17","unstructured":"H\u00fcnke, Y., de Moor, O.: Aiding dependent type checking with rewrite rules (2001) (unpublished), http:\/\/citeseer.ist.psu.edu\/huencke01aiding.html"},{"key":"10_CR18","first-page":"937","volume-title":"OOPSLA 2007 Companion","author":"A. Mametjanov","year":"2007","unstructured":"Mametjanov, A.: Types and program transformations. In: OOPSLA 2007 Companion, pp. 937\u2013938. ACM, New York (2007)"},{"issue":"2","key":"10_CR19","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1017\/S0956796802004550","volume":"13","author":"M.Y. Levin","year":"2003","unstructured":"Levin, M.Y., Pierce, B.C.: TinkerType: A language for playing with formal systems. J. Functional Programing\u00a013(2), 295\u2013316 (2003)","journal-title":"J. Functional Programing"},{"key":"10_CR20","first-page":"173","volume-title":"POPL 2007","author":"D.K. Lee","year":"2007","unstructured":"Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of standard ML. In: POPL 2007, pp. 173\u2013184. ACM, New York (2007)"},{"issue":"4","key":"10_CR21","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. TOPLAS\u00a028(4), 619\u2013695 (2006)","journal-title":"TOPLAS"},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1291151.1291155","volume-title":"ICFP 2007: Proceedings of the 2007 ACM SIGPLAN international conference on Functional programming","author":"P. Sewell","year":"2007","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strni\u0161a, R.: Ott: Effective tool support for the working semanticist. In: ICFP 2007: Proceedings of the 2007 ACM SIGPLAN international conference on Functional programming, pp. 1\u201312. ACM, New York (2007)"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45306-7_26","volume-title":"Compiler Construction","author":"M. Brand van den","year":"2001","unstructured":"van den Brand, M., et al.: The ASF+SDF meta-environment: A component-based language development environment. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol.\u00a02027, p. 365. Springer, Heidelberg (2001)"},{"key":"10_CR24","unstructured":"Ro\u015fu, G.: K: A rewriting-based framework for computations\u2014an informal guide. Technical Report UIUCDCS-R-2007-2926, University of Illinois at Urbana-Champaign (2007)"},{"issue":"1","key":"10_CR25","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. J. TCS\u00a096(1), 73\u2013155 (1992)","journal-title":"J. TCS"},{"issue":"2","key":"10_CR26","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theor. Comput. Sci.\u00a0285(2), 187\u2013243 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlap.2004.03.009","volume":"60-61","author":"G.D. Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming\u00a060-61, 17\u2013139 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"10_CR28","first-page":"9","volume-title":"Specification and validation methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Specification and validation methods, pp. 9\u201336. Oxford University Press Inc., New York (1995)"},{"issue":"1\/2","key":"10_CR29","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1023\/A:1010026413531","volume":"13","author":"C. Strachey","year":"2000","unstructured":"Strachey, C., Wadsworth, C.P.: Continuations: A mathematical semantics for handling full jumps. Higher-Order and Symb. Computation\u00a013(1\/2), 135\u2013152 (2000)","journal-title":"Higher-Order and Symb. Computation"},{"issue":"2","key":"10_CR30","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst.\u00a04(2), 258\u2013282 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR31","unstructured":"Ro\u015fu, G.: K-style Maude definition of the W type inferencer (2007), http:\/\/fsl.cs.uiuc.edu\/index.php\/Special:WOnline"},{"key":"10_CR32","unstructured":"Kothari, S., Caldwell, J.: Algorithm W for lambda calculus extended with Milner-let Implementation used for Type Reconstruction Algorithms\u2014A Survey. Technical Report, University of Wyoming (2007)"},{"key":"10_CR33","unstructured":"Li, Z.: Enhtop: A patch for an enhanced OCaml toplevel (2007), http:\/\/www.pps.jussieu.fr\/~li\/software\/index.html"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Eker, S.: Fast matching in combinations of regular equational theories. In: WRLA 1996. ENTCS, vol.\u00a04, pp. 90\u2013109 (1996)","DOI":"10.1016\/S1571-0661(04)00035-0"},{"key":"10_CR35","unstructured":"Ellison, C.: A rewriting logic approach to defining type systems. Master\u2019s thesis, University of Illinois at Urbana-Champaign (2008), http:\/\/fsl.cs.uiuc.edu\/pubs\/ellison-2008-mastersthesis.pdf"},{"key":"10_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0028739","volume-title":"Computer Aided Verification","author":"R. Hosabettu","year":"1998","unstructured":"Hosabettu, R., Srivas, M.K., Gopalakrishnan, G.: Decomposing the proof of correctness of pipelined microprocessors. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 122\u2013134. Springer, Heidelberg (1998)"},{"key":"10_CR37","first-page":"108","volume-title":"SEFM 2006","author":"A. Kanade","year":"2006","unstructured":"Kanade, A., Sanyal, A., Khedker, U.P.: A PVS based framework for validating compiler optimizations. In: SEFM 2006, pp. 108\u2013117. IEEE Computer Society, Los Alamitos (2006)"},{"key":"10_CR38","series-title":"ENTCS","first-page":"79","volume-title":"COCV 2006","author":"A. Kanade","year":"2007","unstructured":"Kanade, A., Sanyal, A., Khedker, U.P.: Structuring optimizing transformations and proving them sound. In: COCV 2006. ENTCS, vol.\u00a0176(3), pp. 79\u201395. Elsevier, Amsterdam (2007)"},{"key":"10_CR39","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":"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: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03429-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,16]],"date-time":"2024-03-16T04:45:44Z","timestamp":1710564344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03429-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642034282","9783642034299"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03429-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}