{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:39Z","timestamp":1725663819860},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540539049"},{"type":"electronic","value":"9783540463832"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-53904-2_84","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:16:20Z","timestamp":1330208180000},"page":"37-48","source":"Crossref","is-referenced-by-count":6,"title":["Adding algebraic rewriting to the untyped lambda calculus (extended abstract)"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"4_CR1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H. P. Barendregt","year":"1981","unstructured":"H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam. 1981, revised 1984."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"F. Barbanera. Adding Algebraic Rewriting to the Calculus of Constructions: Strong Normalization Preserved. In Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, Concordia University, 1990.","DOI":"10.1007\/3-540-54317-1_96"},{"key":"4_CR3","unstructured":"V. Breazu-Tannen. Conservative extensions of type theories. dissertation, Massachusetts Institute of Technology 1987."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings of the Third Annual Symposium on Logic in Computer Science, pp. 82\u201390. 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"4_CR5","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, to appear."},{"key":"4_CR6","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic confluence. Information and Computation, to appear."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen and A. R. Meyer. Computable values can be classical. In Proceedings of the Fourteenth Symposium on Principles of Programming Languages pp. 238\u2013245, ACM, 1987.","DOI":"10.1145\/41625.41646"},{"issue":"2\/3","key":"4_CR8","first-page":"95","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The Calculus of Constructions. Information and Control, v.76, no.2\/3, pp. 95\u2013120, 1988.","journal-title":"Information and Control"},{"key":"4_CR9","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. J. Symbolic Computation 3, pp. 69\u2013116, 1987.","journal-title":"J. Symbolic Computation"},{"key":"4_CR10","volume-title":"Proc. Second Scandinavian Logic Symposium","author":"J-Y. Girard","year":"1971","unstructured":"J-Y. Girard. Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse, et son application \u00e0 l'elimination des coupures dans l'analyse et la th\u00e9orie des types. In Proc. Second Scandinavian Logic Symposium, ed. J.E. Fenstad. North-Holland, Amsterdam, 1971."},{"key":"4_CR11","unstructured":"J-Y. Girard. Interpr\u00e9tation functionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. These D'Etat, Universite Paris VII, 1972."},{"key":"4_CR12","unstructured":"G. Huet, J.J. L\u00e9vy. Call by need computations in non-ambiguous linear term rewriting systems. Rapport Laboria 359, INRIA, 1979"},{"key":"4_CR13","volume-title":"Formal Languages: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"G. Huet, D. Oppen. Equations and rewrite rules: a survey. In Formal Languages: Perspectives and Open Problems, ed. R. Book. Academic Press, New York 1980."},{"key":"4_CR14","unstructured":"J. W. Klop. Combinatory Reduction Systems. Mathematical Center Tracts 127, Amsterdam, 1980."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"D. B. MacQueen. Using dependent types to express modular structure. In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pp. 277\u2013286, 1986.","DOI":"10.1145\/512644.512670"},{"key":"4_CR16","first-page":"263","volume":"355","author":"A. Middeldorp","year":"1989","unstructured":"A. Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Proc. Third International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 355, pp. 263\u2013277, 1989.","journal-title":"Springer-Verlag LNCS"},{"issue":"3","key":"4_CR17","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1305\/ndjfl\/1093883461","volume":"22","author":"G. Pottinger","year":"1981","unstructured":"G. Pottinger. The Church-Rosser theorem for the typed \u03bb calculus with surjective pairing. Notre Dame Journal of Formal Logic, v.22, no. 3, pp. 264\u2013268, 1981.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"4_CR18","first-page":"408","volume":"19","author":"J. C. Reynolds","year":"1974","unstructured":"J. C. Reynolds. Towards a theory of type structure. In Proc. Colloque sur la Programmation, Springer-Verlag LNCS 19, pp. 408\u2013425, 1974.","journal-title":"Springer-Verlag LNCS"},{"key":"4_CR19","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(87)90039-1","volume":"26","author":"M. Rusinowitch","year":"1987","unstructured":"M. Rusinowitch. On termination of the direct sum of term rewriting systems. Information Processing Letters 26 pp.65\u201370, 1987.","journal-title":"Information Processing Letters"},{"issue":"1","key":"4_CR20","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, v.34, no.1, pp.128\u2013143, 1987.","journal-title":"Journal of the ACM"},{"key":"4_CR21","first-page":"477","volume":"355","author":"Y. Toyama","year":"1989","unstructured":"Y. Toyama, J. W. Klop and H. Barendregt. Termination for the direct sum of left-linear term rewriting systems. In Proc. Third International Conference on Rewriting Techniques and Applications, Springer-Verlag LNCS 355, pp. 477\u2013491, 1989.","journal-title":"Springer-Verlag LNCS"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-53904-2_84.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:51:15Z","timestamp":1605646275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-53904-2_84"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540539049","9783540463832"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-53904-2_84","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}