Editing Lambda calculus (section)

== Further reading ==
* Abelson, Harold & Gerald Jay Sussman. [[Structure and Interpretation of Computer Programs]]. [[The MIT Press]]. {{isbn|0-262-51087-1}}.
* [[Henk Barendregt|Barendregt, Hendrik Pieter]] [http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf ''Introduction to Lambda Calculus''].
* Barendregt, Hendrik Pieter, [https://www.jstor.org/stable/421013 The Impact of the Lambda Calculus in Logic and Computer Science]. The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.
* Barendregt, Hendrik Pieter, ''The Type Free Lambda Calculus'' pp1091–1132 of ''Handbook of Mathematical Logic'', [[North-Holland Publishing Company|North-Holland]] (1977) {{isbn|0-7204-2285-X}}
* Cardone, Felice and Hindley, J. Roger, 2006. [http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf History of Lambda-calculus and Combinatory Logic] {{Webarchive|url=https://web.archive.org/web/20210506154120/http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf |date=2021-05-06}}. In Gabbay and Woods (eds.), ''Handbook of the History of Logic'', vol. 5. Elsevier.
* Church, Alonzo, ''An unsolvable problem of elementary number theory'', [[American Journal of Mathematics]], 58 (1936), pp.&nbsp;345–363. This paper contains the proof that the equivalence of lambda expressions is in general not decidable.
* {{cite book |last1=Church |first1=Alonzo |year=1941 |url=https://archive.org/details/AnnalsOfMathematicalStudies6ChurchAlonzoTheCalculiOfLambdaConversionPrincetonUniversityPress1941 |title=The Calculi of Lambda-Conversion |location=Princeton |publisher=Princeton University Press |access-date=2020-04-14}} ({{isbn|978-0-691-08394-0}})
* {{cite journal|author1-link=Orrin Frink |author=Frink Jr., Orrin |year=1944 |title=Review: ''The Calculi of Lambda-Conversion'' by Alonzo Church |journal=Bulletin of the American Mathematical Society |volume=50 |issue=3 |pages=169–172 |url=https://www.ams.org/bull/1944-50-03/S0002-9904-1944-08090-7/S0002-9904-1944-08090-7.pdf|doi=10.1090/s0002-9904-1944-08090-7 |doi-access=free}}
* Kleene, Stephen, ''A theory of positive integers in formal logic'', [[American Journal of Mathematics]], 57 (1935), pp.&nbsp;153–173 and 219–244. Contains the lambda calculus definitions of several familiar functions.
* [[Peter Landin|Landin, Peter]], ''A Correspondence Between ALGOL 60 and Church's Lambda-Notation'', [[Communications of the ACM]], vol. 8, no. 2 (1965), pages 89–101. Available from the [http://portal.acm.org/citation.cfm?id=363749&coll=portal&dl=ACM ACM site]. A classic paper highlighting the importance of lambda calculus as a basis for programming languages.
* Larson, Jim, [https://web.archive.org/web/20011206080336/http://www.jetcafe.org/~jim/lambda.html ''An Introduction to Lambda Calculus and Scheme'']. A gentle introduction for programmers.
*{{cite book |last1=Michaelson |first1=Greg |title=An Introduction to Functional Programming Through Lambda Calculus |date=10 April 2013 |publisher=Courier Corporation |isbn=978-0-486-28029-5 |language=en}}<ref>{{cite web |title=Greg Michaelson's Homepage |url=http://www.macs.hw.ac.uk/~greg/ |website=Mathematical and Computer Sciences |publisher=[[Heriot-Watt University]] |access-date=6 November 2022 |location=Riccarton, Edinburgh}}</ref>
* Schalk, A. and Simmons, H. (2005) ''[https://web.archive.org/web/20080307014129/http://www.cs.man.ac.uk/~hsimmons/BOOKS/lcalculus.pdf An introduction to λ-calculi and arithmetic with a decent selection of exercises]''. Notes for a course in the Mathematical Logic MSc at Manchester University.
* {{cite journal|last1=de Queiroz|first1=Ruy J.G.B.|author1-link=Ruy de Queiroz|year=2008|title=On Reduction Rules, Meaning-as-Use and Proof-Theoretic Semantics|journal=[[Studia Logica]]|volume=90|issue=2|pages=211–247|doi=10.1007/s11225-008-9150-5|s2cid=11321602}} A paper giving a formal underpinning to the idea of 'meaning-is-use' which, even if based on proofs, it is different from proof-theoretic semantics as in the Dummett–Prawitz tradition since it takes reduction as the rules giving meaning.
* Hankin, Chris, ''An Introduction to Lambda Calculi for Computer Scientists,'' {{isbn|0954300653}}

;Monographs/textbooks for graduate students:
* Sørensen, Morten Heine and Urzyczyn, Paweł (2006), ''Lectures on the Curry–Howard isomorphism'', Elsevier, {{isbn|0-444-52077-5}} is a recent monograph that covers the main topics of lambda calculus from the type-free variety, to most [[typed lambda calculi]], including more recent developments like [[pure type system]]s and the [[lambda cube]]. It does not cover [[subtyping]] extensions.
* {{Citation|last1=Pierce|first1=Benjamin|title=Types and Programming Languages|publisher=MIT Press|year=2002|isbn=0-262-16209-1}} covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.

;Documents
* ''[http://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf A Short Introduction to the Lambda Calculus]''-([[Portable Document Format|PDF]]) by Achim Jung
* ''[http://turing100.acm.org/lambda_calculus_timeline.pdf A timeline of lambda calculus]''-([[Portable Document Format|PDF]]) by Dana Scott
* ''[http://www.inf.fu-berlin.de/inst/ag-ki/rojas_home/documents/tutorials/lambda.pdf A Tutorial Introduction to the Lambda Calculus]''-([[Portable Document Format|PDF]]) by Raúl Rojas
* ''[http://www.mscs.dal.ca/~selinger/papers/#lambdanotes Lecture Notes on the Lambda Calculus]''-([[Portable Document Format|PDF]]) by Peter Selinger
* [https://web.archive.org/web/20140202195546/http://imar.ro/~mbuliga/graphic_revised.pdf ''Graphic lambda calculus''] by Marius Buliga
* [https://web.archive.org/web/20160729210437/http://cs.adelaide.edu.au/~pmk/publications/wage2008.pdf ''Lambda Calculus as a Workflow Model''] by Peter Kelly, Paul Coddington, and Andrew Wendelborn; mentions [[graph reduction]] as a common means of evaluating lambda expressions and discusses the applicability of lambda calculus for [[distributed computing]] (due to the [[Church–Rosser theorem|Church–Rosser]] property, which enables [[parallel computing|parallel]] graph reduction for lambda expressions).