{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:07:29Z","timestamp":1725487649518},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426721"},{"type":"electronic","value":"9783540454465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45446-2_3","type":"book-chapter","created":{"date-parts":[[2007,7,22]],"date-time":"2007-07-22T22:11:27Z","timestamp":1185142287000},"page":"38-49","source":"Crossref","is-referenced-by-count":0,"title":["Confluence of Untyped Lambda Calculus via Simple Types"],"prefix":"10.1007","author":[{"given":"Silvia","family":"Ghilezan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,10,16]]},"reference":[{"key":"3_CR1","volume-title":"The Lambda Calculus-Its Syntax and Semantics","author":"H. P. Barendregt","year":"1984","unstructured":"Barendregt, H. P.: The Lambda Calculus-Its Syntax and Semantics. North-Holland, Amsterdam (1984)."},{"key":"3_CR2","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H. P. Barendregt","year":"1992","unstructured":"Barendregt, H. P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D. M. and T. S. E. Maibaum (eds.): Handbook of Logic in Computer Science, Vol. 2. Oxford University Press, Oxford (1992) 117\u2013309."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. and J. P. Jounnaud: Rewrite Systems. In: Leeuwen, J. (ed.): Handbook of Theoretical Computer Science, Elsevier Science Publishers B. V. (1990).","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"3_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/3-540-58140-5_13","volume-title":"Logical Foundations of Computer Science\u2019 94","author":"S. Ghilezan","year":"1994","unstructured":"Ghilezan, S.: Application of typed lambda calculi in the untyped lambda calculus. In: Nerode, A. and Yu. Matiyasevich (eds.): Logical Foundations of Computer Science\u2019 94. Lecture Notes in Computer Science 813, Springer-Verlag, Berlin (1994) 129\u2013139."},{"key":"3_CR5","first-page":"247","volume":"4","author":"S. Ghilezan","year":"1996","unstructured":"Ghilezan, S.: Generalized finiteness of developments in typed lambda calculi. Journal of Automata, Languages and Combinatorics 4 (1996) 247\u2013257.","journal-title":"Journal of Automata, Languages and Combinatorics"},{"issue":"3","key":"3_CR6","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1093\/logcom\/10.3.437","volume":"10","author":"J. W. Klop","year":"2000","unstructured":"Klop, J. W., V. van Oostrom, and R. de Vrijer: A geometric proof of confluence by decreasing diagrams. Journal of Logic and Computation 10(3) (2000) 437\u2013460.","journal-title":"Journal of Logic and Computation"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"782","DOI":"10.2307\/2274330","volume":"50","author":"G. Koletsos","year":"1985","unstructured":"Koletsos, G.: Church-Rosser theorem for typed functionals. Journal of Symbolic Logic 50 (1985) 782\u2013790.","journal-title":"Journal of Symbolic Logic"},{"key":"3_CR8","unstructured":"Koletsos, G. and G. Stavrinos: Church-Rosser theorem for conjunctive type systems. In: Kakas, A. K. and A. Sinachopoulos (eds.): Proceedings of the First Panhellenic Logic Symposium. Nicosia (1997) 25\u201337."},{"key":"3_CR9","volume-title":"Lambda-calcul types et mod\u00e8les","author":"J. L. Krivine","year":"1990","unstructured":"Krivine, J. L.: Lambda-calcul types et mod\u00e8les. Masson, Paris (1990)"},{"key":"3_CR10","first-page":"52","volume":"122","author":"A. M. Meyer","year":"1982","unstructured":"Meyer, A. M.: What is a model of lambda calculus? Information and control 122 (1982) 52\u201387.","journal-title":"Information and control"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Mitchell, J.: Type Systems for Programming Languages. In: Leeuwen, J. (ed.): Handbook of Theoretical Computer Science, Elsevier Science Publishers B. V. (1990) 365\u2013458.","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M. H. A. Newman","year":"1942","unstructured":"Newman, M. H. A.: On theories with a combinatorial definition of \u2018equivalence\u2019. Annals of Mathematics 43 (1942) 223\u2013243.","journal-title":"Annals of Mathematics"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: A Proof of the Church-Rosser theorem and its representation in a Logical Framework, CMU-CS-92-186, (September 1992), forthocoming in Journal of Authomated Reasoning.","DOI":"10.21236\/ADA256574"},{"key":"3_CR14","first-page":"403","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"D. Scott","year":"1980","unstructured":"Scott, D.: Relating theories of the lambda calculus. In: Seldin, J. P. and J. R. Hindley: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London (1980) 403\u2013450."},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"Statman, R.: Logical relations and the simply typed lambda calculus. Information and Control 65 (1985) 85\u201397.","journal-title":"Information and Control"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0747-7171(89)80045-8","volume":"7","author":"M. Takahashi","year":"1989","unstructured":"Takahashi, M.: Parallel Reductions in \u03bb-Calculus. Journal of Symbolic Computation 7 (1989) 113\u2013123.","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/0304-3975(92)00023-K","volume":"126","author":"V. Oostrom van","year":"1994","unstructured":"van Oostrom, V.: Confluence by decreasing diagrams. Theoretical Computer Science 126 (1994) 259\u2013280.","journal-title":"Theoretical Computer Science"},{"key":"3_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/3-540-58140-5_35","volume-title":"Logical Foundations of Computer Science\u2019 94","author":"V. Oostrom van","year":"1994","unstructured":"van Oostrom, V. and F. van Raamsdonk: Weak orthogonality implies confluence: the higher order case. In: Nerode, A. and Yu. Matiyasevich (eds.): Logical Foundations of Computer Science\u2019 94. Lecture Notes in Computer Science 813, Springer-Verlag, Berlin (1994) 379\u2013392."},{"issue":"3","key":"3_CR19","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1137\/0205036","volume":"5","author":"C. P. Wadsworth","year":"1976","unstructured":"Wadsworth, C. P.: The relation between computational and denotational properties for Scott\u2019s D\u221e-models of the lambda calculus. SIAM Journal of Computing 5(3) (1976) 488\u2013521.","journal-title":"SIAM Journal of Computing"}],"container-title":["Lecture Notes in Computer Science","Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45446-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T07:42:29Z","timestamp":1556696549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45446-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426721","9783540454465"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45446-2_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}