{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T21:45:34Z","timestamp":1768340734449,"version":"3.49.0"},"reference-count":119,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":6072,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[1997,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the representation of computations and the resulting functional programming languages on the one hand and the representation of reasoning and the resulting systems of computer mathematics on the other hand.<\/jats:p>","DOI":"10.2307\/421013","type":"journal-article","created":{"date-parts":[[2006,5,7]],"date-time":"2006-05-07T07:10:12Z","timestamp":1146985812000},"page":"181-215","source":"Crossref","is-referenced-by-count":50,"title":["The Impact of the Lambda Calculus in Logic and Computer Science"],"prefix":"10.1017","volume":"3","author":[{"given":"Henk","family":"Barendregt","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600007599_ref059","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley","year":"1969","journal-title":"Transactions of the American Mathematical Society"},{"key":"S1079898600007599_ref053","first-page":"1","volume-title":"Theoretical Computer Science","author":"Grue","year":"1992"},{"key":"S1079898600007599_ref107","doi-asserted-by":"publisher","DOI":"10.1137\/0211062"},{"key":"S1079898600007599_ref014","doi-asserted-by":"crossref","unstructured":"Barendsen E. and Smetsers J. E. W. , Conventional and uniqueness typing in graph rewrite systems (extended abstract), 1993, in [105], pp. 41\u201351.","DOI":"10.1007\/3-540-57529-4_42"},{"key":"S1079898600007599_ref034","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90020-7"},{"key":"S1079898600007599_ref007","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1017\/S0956796800020062","article-title":"Theoretical pearls: Self-interpretation in lambda calculus","volume":"1","author":"Barendregt","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"S1079898600007599_ref040","volume-title":"Functional programming and parallel graph rewriting","author":"van Eekelen","year":"1993"},{"key":"S1079898600007599_ref051","volume-title":"Proofs and types","volume":"7","author":"Girard","year":"1989"},{"key":"S1079898600007599_ref041","unstructured":"Elbers H. , Personal communication, 1996."},{"key":"S1079898600007599_ref044","doi-asserted-by":"publisher","DOI":"10.1007\/BF01135376"},{"key":"S1079898600007599_ref060","volume-title":"The enigma of intelligence","author":"Hodges","year":"1983"},{"key":"S1079898600007599_ref099","first-page":"216","volume-title":"ACM symposium on Lisp and functional programming","author":"Rosser","year":"1982"},{"key":"S1079898600007599_ref054","first-page":"633","article-title":"Semantic domains","volume":"B","author":"Gunter","year":"1990","journal-title":"Handbook of theoretical computer science"},{"key":"S1079898600007599_ref005","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359579"},{"key":"S1079898600007599_ref018","unstructured":"Jutting L. S. van Benthem , Checking Landau's \u201cGrundlagen\u201d in the AUTOMATH system, Ph.D. thesis , Eindhoven University of Technology, 1977."},{"key":"S1079898600007599_ref016","volume-title":"Foundations of constructive mathematics","author":"Beeson","year":"1980"},{"key":"S1079898600007599_ref074","first-page":"17","article-title":"The formalist-positivist doctrine of mathematical precision in the light of experience","volume":"3","author":"Kreisel","year":"1970","journal-title":"L'age de la Science"},{"key":"S1079898600007599_ref109","volume-title":"Technical Report AI-TR-474","author":"Steele","year":"1978"},{"key":"S1079898600007599_ref077","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"S1079898600007599_ref106","first-page":"302","article-title":"Begr\u00fcndung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Ver\u00ebnderlichen mit unendlichem Ausdehnungsbereich","volume":"6","author":"Skolem","year":"1923","journal-title":"Videnskapsselskapets skrifter, I. Matematisk-naturvidenskabelig klasse"},{"key":"S1079898600007599_ref092","first-page":"71","volume-title":"Conference record ofthe twentieth annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, Charleston, South Carolina, January 10-13, 1992","author":"Jones","year":"1993"},{"key":"S1079898600007599_ref017","volume-title":"Language in action: Categories, lambdas and dynamic logic","volume":"130","author":"van Benthem","year":"1991"},{"key":"S1079898600007599_ref100","volume-title":"Principia mathematica","volume":"2","author":"Russell","year":"1910"},{"key":"S1079898600007599_ref020","doi-asserted-by":"crossref","unstructured":"Bezem M. and Groote J. F. (editors), Typed lambda calculi and applications, TLCA'93, Lecture Notes in Computer Science, vol. 664, Berlin and New York, Springer-Verlag, 1993.","DOI":"10.1007\/BFb0037093"},{"key":"S1079898600007599_ref080","volume-title":"Technical Report ECS-LFCS-92-211","author":"Luo","year":"1992"},{"key":"S1079898600007599_ref012","unstructured":"Barendregt H. P. and Barendsen E. , Efficient computations in formal proofs, to appear, 1997."},{"key":"S1079898600007599_ref108","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90007-0"},{"key":"S1079898600007599_ref085","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000423"},{"key":"S1079898600007599_ref104","first-page":"316","volume-title":"Proceedings of LFCS'94","volume":"813","author":"Severi","year":"1994"},{"key":"S1079898600007599_ref079","first-page":"460","volume-title":"24th annual symposium on foundations of computer science","author":"Leivant","year":"1983"},{"key":"S1079898600007599_ref004","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561307"},{"key":"S1079898600007599_ref021","first-page":"179","volume-title":"Annual review in automatic programming","volume":"3","author":"B\u00f6hm","year":"1963"},{"key":"S1079898600007599_ref070","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.1981.10004"},{"key":"S1079898600007599_ref062","first-page":"R1","article-title":"Report on the programming language Haskell: A non-strict, purely functional language (Version 1.2)","volume":"27","author":"Hudak","year":"1992","journal-title":"ACM SIGPLAN Notices"},{"key":"S1079898600007599_ref082","first-page":"89","volume-title":"Fourth international congress for logic, methodology and philosophy of science","volume":"74","author":"Matijasevi\u010d","year":"1971"},{"key":"S1079898600007599_ref030","volume-title":"The calculi of lambda conversion","author":"Church","year":"1941"},{"key":"S1079898600007599_ref073","doi-asserted-by":"crossref","unstructured":"Kreisel G. , Church's thesis: A kind of reducibility axiom for constructive mathematics, in [86], pp. 121\u2013150.","DOI":"10.1016\/S0049-237X(08)70746-8"},{"key":"S1079898600007599_ref118","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-15975-4_26","volume-title":"Functional programming languages and computer architectures","volume":"201","author":"Turner","year":"1985"},{"key":"S1079898600007599_ref045","volume-title":"Logic, language and meaning","author":"Gamut","year":"1992"},{"key":"S1079898600007599_ref057","volume-title":"Functional programming: Application and implementation","author":"Henderson","year":"1980"},{"key":"S1079898600007599_ref023","first-page":"35","volume-title":"Automata theory","author":"B\u00f6hm","year":"1966"},{"key":"S1079898600007599_ref116","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380090105"},{"key":"S1079898600007599_ref112","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S1079898600007599_ref102","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060636"},{"key":"S1079898600007599_ref042","unstructured":"Euclid , The elements, 325 B.C. English translation in [55], 1956."},{"key":"S1079898600007599_ref114","doi-asserted-by":"publisher","DOI":"10.2307\/2268280"},{"key":"S1079898600007599_ref105","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57529-4"},{"key":"S1079898600007599_ref050","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150"},{"key":"S1079898600007599_ref049","unstructured":"Girard J.-Y. , Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, Ph.D. thesis , Universite Paris VII, 1972."},{"key":"S1079898600007599_ref086","volume-title":"Intuitionism and proof theory","author":"Myhill","year":"1970"},{"key":"S1079898600007599_ref063","unstructured":"Hughes R. J. M. , The design and implementation of programming languages, Ph.D. thesis , University of Oxford, 1984."},{"key":"S1079898600007599_ref084","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S1079898600007599_ref024","first-page":"135","volume-title":"Esop'94","volume":"788","author":"B\u00f6hm","year":"1994"},{"key":"S1079898600007599_ref035","volume-title":"Categorical combinators, sequential algorithms, and functional programming","author":"Curien","year":"1986"},{"key":"S1079898600007599_ref038","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01183.x"},{"key":"S1079898600007599_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)00022-U"},{"key":"S1079898600007599_ref075","first-page":"104","volume-title":"Information and Computation","author":"Kuper","year":"1993"},{"key":"S1079898600007599_ref028","doi-asserted-by":"publisher","DOI":"10.2307\/2371045"},{"key":"S1079898600007599_ref011","first-page":"39","volume-title":"Images of SMC research","author":"Barendregt","year":"1996"},{"key":"S1079898600007599_ref087","first-page":"810","volume-title":"Logic programming: Proceedings of the fifth international conference and symposium, Volume 1","author":"Nadathur","year":"1988"},{"key":"S1079898600007599_ref083","doi-asserted-by":"crossref","DOI":"10.21236\/AD0406138","volume-title":"Lisp 1.5 programmer's manual","author":"McCarthy","year":"1962"},{"key":"S1079898600007599_ref009","first-page":"141","volume-title":"From universal morphisms to megabytes: A Baayen space-odyssey","author":"Barendregt","year":"1994"},{"key":"S1079898600007599_ref025","volume-title":"F. P. Ramsay: The foundations of mathematics and other logical essays","author":"Braithwaite","year":"1960"},{"key":"S1079898600007599_ref065","doi-asserted-by":"publisher","DOI":"10.1145\/1460833.1460872"},{"key":"S1079898600007599_ref032","volume-title":"Revised report on the algorithmic language Scheme","volume":"IV","author":"Clinger","year":"1991"},{"key":"S1079898600007599_ref037","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.20.11.584"},{"key":"S1079898600007599_ref027","doi-asserted-by":"crossref","unstructured":"de Bruijn N. G. , Reflections on Automath, Eindhoven University of Technology, 1990, also in [88], pp. 201\u2013228.","DOI":"10.1016\/S0049-237X(08)70205-2"},{"key":"S1079898600007599_ref031","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"key":"S1079898600007599_ref048","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"S1079898600007599_ref006","volume-title":"The lambda calculus: its syntax and semantics","author":"Barendregt","year":"1984"},{"key":"S1079898600007599_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"S1079898600007599_ref067","doi-asserted-by":"publisher","DOI":"10.1215\/S0012-7094-36-00227-2"},{"key":"S1079898600007599_ref076","volume-title":"Grundlagen der analysis","author":"Landau","year":"1960"},{"key":"S1079898600007599_ref026","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060623"},{"key":"S1079898600007599_ref033","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S1079898600007599_ref058","volume-title":"Grundz\u00fcge der theoretischen logik","volume":"XXVII","author":"Hilbert","year":"1928"},{"key":"S1079898600007599_ref036","first-page":"789","volume-title":"American Journal of Mathematics","volume":"52","author":"Curry","year":"1930"},{"key":"S1079898600007599_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BF01459088"},{"key":"S1079898600007599_ref064","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.98"},{"key":"S1079898600007599_ref055","volume-title":"The thirteen books of Euclid's elements","author":"Heath","year":"1956"},{"key":"S1079898600007599_ref047","unstructured":"Gentzen G. , Investigations into logical deduction, in [111], 1969."},{"key":"S1079898600007599_ref068","volume-title":"Introduction to metamathematics","author":"Kleene","year":"1952"},{"key":"S1079898600007599_ref008","first-page":"117","volume-title":"Lambda calculi with types","author":"Barendregt","year":"1992"},{"key":"S1079898600007599_ref088","volume-title":"Selected papers on automath","volume":"133","author":"Nederpelt","year":"1994"},{"key":"S1079898600007599_ref015","volume-title":"Mathematical Structures in Computer Science","author":"Barendsen","year":"1997"},{"key":"S1079898600007599_ref081","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S1079898600007599_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56992-8_7"},{"key":"S1079898600007599_ref066","doi-asserted-by":"publisher","DOI":"10.1145\/502949.502880"},{"key":"S1079898600007599_ref039","article-title":"Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic","author":"Dekkers","year":"1997","journal-title":"Journal of Symbolic Logic"},{"key":"S1079898600007599_ref043","first-page":"87","volume-title":"Proof theory symposium","volume":"500","author":"Feferman","year":"1975"},{"key":"S1079898600007599_ref052","volume-title":"Functional programming and Input\/Output","author":"Gordon","year":"1994"},{"key":"S1079898600007599_ref003","volume-title":"Compiling with continuations","author":"Appel","year":"1992"},{"key":"S1079898600007599_ref013","doi-asserted-by":"publisher","DOI":"10.2307\/2275096"},{"key":"S1079898600007599_ref078","volume-title":"Handbook of theoretical computer science","volume":"B","author":"van Leeuwen","year":"1990"},{"key":"S1079898600007599_ref072","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)90796-3"},{"key":"S1079898600007599_ref046","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71257-6"},{"key":"S1079898600007599_ref103","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0073967"},{"key":"S1079898600007599_ref071","doi-asserted-by":"publisher","DOI":"10.2307\/1968646"},{"key":"S1079898600007599_ref101","first-page":"113","article-title":"Definierbare Funktionen im \u03bb-Kalk\u00fcl mit Typen","volume":"25","author":"Schwichtenberg","year":"1976","journal-title":"Archief f\u00fcr Mathematische Logik"},{"key":"S1079898600007599_ref113","first-page":"230","article-title":"On computable numbers with an application to the Entscheidungsproblem","volume":"42","author":"Turing","year":"1936","journal-title":"Proceeding of the London Mathematical Society. Second Series."},{"key":"S1079898600007599_ref069","first-page":"1","volume-title":"Algebra and logic (Fourteenth summer res. inst., Austral. Math. Soc., Monash Univ., Clayton, 1974)","volume":"450","author":"Kleene","year":"1975"},{"key":"S1079898600007599_ref117","first-page":"85","volume-title":"Proceedings of the ACM\/MIT conference on functional languages and computer architecture","author":"Turner","year":"1981"},{"key":"S1079898600007599_ref094","volume-title":"La science et l'hypoth\u00e8se","author":"Poincar\u00e9","year":"1902"},{"key":"S1079898600007599_ref091","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring C. , Inductive definitions in the system Coq; rules and properties, 1993, in [20], pp. 328\u2013345.","DOI":"10.1007\/BFb0037116"},{"key":"S1079898600007599_ref056","volume-title":"From Frege to G\u00f6del: A source book in mathematical logic, 1879\u20131931","author":"van Heijenoort","year":"1967"},{"key":"S1079898600007599_ref061","first-page":"216","volume-title":"Typed lambda calculi and applications","author":"Hofmann","year":"1977"},{"key":"S1079898600007599_ref097","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019459"},{"key":"S1079898600007599_ref095","first-page":"338","article-title":"The foundations of mathematics","volume":"25","author":"Ramsey","year":"1925","journal-title":"Proceedings of the London Mathematical Society, Series 2"},{"key":"S1079898600007599_ref115","unstructured":"Turner D. A. , The SASL language manual, 1976."},{"key":"S1079898600007599_ref029","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S1079898600007599_ref001","volume-title":"Handbook of logic in computer science, Volume 2: Background: Computational structures","author":"Abramsky","year":"1992"},{"key":"S1079898600007599_ref098","doi-asserted-by":"publisher","DOI":"10.1017\/S0022481200039463"},{"key":"S1079898600007599_ref111","volume-title":"The collected papers of Gerhard Gentzen","author":"Szabo","year":"1969"},{"key":"S1079898600007599_ref090","unstructured":"Oostdijk M. , Proof by calculation, Master's thesis, 385 , Universitaire School voor Informatica, Catholic University Nijmegen, 1996."},{"key":"S1079898600007599_ref096","first-page":"717","volume-title":"Proceedings of 25th ACM national conference","author":"Reynolds","year":"1972"},{"key":"S1079898600007599_ref089","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1515\/crll.1925.154.219","article-title":"Eine axiomatisierung der mengenlehre","volume":"154","author":"von Neumann","year":"1925","journal-title":"Journal f\u00fcr die Reine und Angewandte Mathematik"},{"key":"S1079898600007599_ref119","unstructured":"Wadswortt C. , Semantics and pragmatics of the lambda-calculus, D. Phil thesis , University of Oxford, Programming Research Group, Oxford, U.K., 1971."},{"key":"S1079898600007599_ref093","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S1079898600007599_ref110","volume-title":"Common Lisp: The language","author":"Steele","year":"1984"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600007599","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,7]],"date-time":"2023-05-07T10:16:32Z","timestamp":1683454592000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600007599\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,6]]},"references-count":119,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,6]]}},"alternative-id":["S1079898600007599"],"URL":"https:\/\/doi.org\/10.2307\/421013","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,6]]}}}