{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,12]],"date-time":"2024-12-12T05:54:21Z","timestamp":1733982861582,"version":"3.30.2"},"reference-count":23,"publisher":"Duke University Press","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Notre Dame J. Formal Logic"],"published-print":{"date-parts":[[1994,10,1]]},"DOI":"10.1305\/ndjfl\/1040408614","type":"journal-article","created":{"date-parts":[[2003,2,25]],"date-time":"2003-02-25T21:37:13Z","timestamp":1046209033000},"source":"Crossref","is-referenced-by-count":2,"title":["Normal Forms in Combinatory Logic"],"prefix":"10.1215","volume":"35","author":[{"given":"Patricia","family":"Johann","sequence":"first","affiliation":[]}],"member":"73","reference":[{"key":"1","unstructured":"Barendregt, H., <i>The Lambda Calculus, Its Syntax and Semantics<\/i>, North-Holland, Amsterdam, 1984. Zbl 0551.03007 MR 86a:03012"},{"key":"2","doi-asserted-by":"crossref","unstructured":"Breazu-Tannen V., \u201cCombining algebra and higher-order types,\u201d pp. 82\u201390 in <i>Proceedings of the Third Annual Symposium on Logic in Computer Science<\/i>, 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"3","doi-asserted-by":"crossref","unstructured":"Breazu-Tannen, V., and J. Gallier, \u201cPolymorphic rewriting conserves algebraic strong normalization,\u201d <i>Theoretical Computer Science<\/i>, vol. 83 (1991), pp. 3\u201328. Zbl 0745.68065","DOI":"10.1016\/0304-3975(91)90037-3"},{"key":"4","doi-asserted-by":"publisher","unstructured":"Breazu-Tannen, V., and J. Gallier, \u201cPolymorphic rewriting conserves algebraic confluence,\u201d <i>Information and Computation<\/i>, vol. 114 (1994), pp. 1\u201329. Zbl 0820.68059 MR 95i:68066","DOI":"10.1006\/inco.1994.1078"},{"key":"5","unstructured":"Curry, H., and R. Feys, <i>Combinatory Logic, Vol. I<\/i>, North-Holland, Amsterdam, 1958. Zbl 0081.24104 MR 20:817"},{"key":"6","unstructured":"Curry, H., J. Hindley and J. Seldin, <i>Combinatory Logic, Vol. II<\/i>, North-Holland, Amsterdam, 1972. Zbl 0242.02029"},{"key":"7","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., and J.-P. Jouannaud, \u201cRewrite systems,\u201d pp. 243\u2013320 in <i>Handbook of Theoretical Computer Science B: Formal Methods and Semantics<\/i>, edited by J. van Leeuwen, North-Holland, Amsterdam, 1990. Zbl 0900.68283 MR 1127191","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"8","doi-asserted-by":"crossref","unstructured":"Dougherty, D., \u201cAdding algebraic rewriting to the untyped lambda calculus,\u201dpp. 37\u201348 in <i>Proceedings of the Fourth International Conference on Rewriting Techniques and Applications<\/i>, Springer-Verlag LNCS 488, 1991. Also appears in <i>Information and Computation<\/i>, vol. 101, 102 (1992), pp. 251\u2013267. Zbl 0769.68058 MR 94g:68060","DOI":"10.1016\/0890-5401(92)90064-M"},{"key":"9","doi-asserted-by":"crossref","unstructured":"Dougherty, D., and P. Johann, \u201cA combinatory logic approach to higher-order $E$-unification,\u201d pp. 79\u201393 in <i>Proceedings of the Eleventh International Conference on Automated Deduction<\/i>, Springer-Verlag LNAI 607, 1992. Expanded version appears in <i>Theoretical Computer Science<\/i>, vol. 139 (1995), pp. 207-242. Zbl 0874.68271 MR 96d:68113","DOI":"10.1016\/0304-3975(94)00210-A"},{"key":"10","doi-asserted-by":"crossref","unstructured":"Gallier, J., and W. Snyder, \u201cHigher-order unification revisited: complete sets of transformations,\u201d <i>Journal of Symbolic Computation<\/i>, vol. 8 (1989), pp. 101\u2013140. Zbl 0682.03034 MR 90j:03025","DOI":"10.1016\/S0747-7171(89)80023-9"},{"key":"11","doi-asserted-by":"publisher","unstructured":"Hindley, R., \u201cAxioms for strong reduction in combinatory logic,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 32 (1967), pp. 224\u2013236. Zbl 0153.00603 MR 35:5320","DOI":"10.2307\/2271660"},{"key":"12","doi-asserted-by":"publisher","unstructured":"Hindley, R., \u201cCombinatory reductions and lambda reductions compared,\u201d <i>Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik<\/i>, vol. 23 (1977), pp. 169\u2013180. Zbl 0361.02035 MR 58:5080","DOI":"10.1002\/malq.19770230708"},{"key":"13","doi-asserted-by":"crossref","unstructured":"Hindley, R., and B. Lercher, \u201cA short proof of Curry's normal form theorem,\u201dpp. 808\u2013810 in <i>Proceedings of the American Mathematical Society<\/i>, vol. 24, 1970. Zbl 0195.02101 MR 41:67","DOI":"10.2307\/2037329"},{"key":"14","unstructured":"Hindley, J., B. Lercher, and J. Seldin, <i>Introduction to Combinatory Logic<\/i>, Cambridge University Press, Cambridge, 1972. Zbl 0269.02005 MR 49:25"},{"key":"15","unstructured":"Hindley, J., and J. Seldin. <i>Introduction to Combinators and $\\lambda$-Calculus<\/i>, Cambridge University Press, Cambridge, 1986. Zbl 0614.03014 MR 88j:03009"},{"key":"16","doi-asserted-by":"crossref","unstructured":"Huet, G., \u201cA unification algorithm for typed $\\lambda$-calculus,\u201d <i>Theoretical Computer Science<\/i>, vol. 1 (1975), pp. 27\u201357. Zbl 0337.68027","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"17","unstructured":"Johann, P., <i>Complete sets of transformations for unification problems<\/i>, Dissertation, Wesleyan University, 1991."},{"key":"18","unstructured":"Johann, P., \u201cNormal forms in combinatory logic,\u201d Technical Report, Wesleyan University, 1992. Zbl 0830.03005 MR 96d:03025"},{"key":"19","unstructured":"Klop, J., \u201cCombinatory reduction systems,\" <i>Mathematical Center Tracts<\/i> 129, Amsterdam, 1980. Zbl 0466.03006 MR 83e:03026"},{"key":"20","doi-asserted-by":"publisher","unstructured":"Lercher, B., \u201cThe decidability of Hindley's axioms for strong reduction,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 32 (1967), pp. 237\u2013239. Zbl 0153.00701 MR 35:5321","DOI":"10.2307\/2271661"},{"key":"21","doi-asserted-by":"publisher","unstructured":"Lercher, B., \u201cStrong reduction and normal forms in combinatory logic,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 32 (1967), pp. 213\u2013223. MR 36:2505","DOI":"10.2307\/2271659"},{"key":"22","doi-asserted-by":"crossref","unstructured":"Mezghiche, M., \u201cOn pseudo-$c\\beta$ normal form in combinatory logic,\u201d <i>Theoretical Computer Science<\/i>, vol. 66 (1989), pp. 323\u2013331. Zbl 0673.03010 MR 91e:03018","DOI":"10.1016\/0304-3975(89)90157-6"},{"key":"23","doi-asserted-by":"crossref","unstructured":"R\u00e9ty, P., \u201cImproving basic narrowing techniques,\u201d pp. 228-241 in <i>Proceedings of the Second International Conference on Rewriting Techniques and Applications<\/i>, 1987. Zbl 0638.68101 MR 903675","DOI":"10.1007\/3-540-17220-3_20"}],"container-title":["Notre Dame Journal of Formal Logic"],"original-title":[],"link":[{"URL":"https:\/\/projecteuclid.org\/journalArticle\/Download?urlid=10.1305\/ndjfl\/1040408614","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,11]],"date-time":"2024-12-11T21:50:35Z","timestamp":1733953835000},"score":1,"resource":{"primary":{"URL":"https:\/\/projecteuclid.org\/journals\/notre-dame-journal-of-formal-logic\/volume-35\/issue-4\/Normal-Forms-in-Combinatory-Logic\/10.1305\/ndjfl\/1040408614.full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,10,1]]},"references-count":23,"journal-issue":{"issue":"4","published-online":{"date-parts":[[1994,10,1]]}},"URL":"https:\/\/doi.org\/10.1305\/ndjfl\/1040408614","relation":{},"ISSN":["0029-4527"],"issn-type":[{"type":"print","value":"0029-4527"}],"subject":[],"published":{"date-parts":[[1994,10,1]]}}}