Lambda calculus (often written λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It was introduced by Alonzo Church in the 1930s, reaching its mature form in his 1936 paper "An Unsolvable Problem of Elementary Number Theory" [2], and despite a grammar with only three constructs (variables, abstractions, and applications) it is a Turing-complete (universal) model of computation. Together with the Turing machine, it is one of the two classical formalizations of the notion of an effectively calculable function, and the equivalence of the two underlies the Church-Turing thesis [18].

Lambda calculus is the theoretical foundation of functional programming. Its concepts of higher-order functions, substitution, and reduction directly inspired LISP (designed by John McCarthy in 1958, published in 1960) [8] and the family of statically typed functional languages including ML, OCaml, and Haskell. Its typed variants, from the simply typed lambda calculus through dependently typed systems, form the basis of modern type theory and the proof assistants used to formally verify mathematics and software.

Infobox

Field	Value
Introduced by	Alonzo Church
First published	1932 (initial system); 1936 (consistent core); 1941 (textbook treatment)
Type	Formal system; model of computation
Computational power	Turing-complete
Type systems	Untyped, simply typed, polymorphic (System F), dependently typed
Influenced	LISP, ML, Scheme, Standard ML, Miranda, Haskell, OCaml, F#, Scala, Clojure
Notable theorems	Church-Rosser theorem; Church-Turing thesis; undecidability of beta-equivalence
Related formalisms	Combinatory logic; Turing machines; recursive functions

What is the lambda calculus?

The lambda calculus is, in the words of the Stanford Encyclopedia of Philosophy, "at heart, a simple notation for functions and application" [17]. Everything in it is a function: there are no built-in numbers, booleans, lists, conditionals, loops, or recursion, yet "all computable (number-theoretic) functions can be faithfully represented in the λ-calculus" [17]. It is, in this sense, exactly as expressive as Turing machines and the general recursive functions, which is why it is described as Turing-complete.

A single, quotable sentence captures both the calculus and its computational reach. Church proposed in 1936 to "define the notion ... of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers (or of a λ-definable function of positive integers)" [18]. That proposal, made before Turing's machine model appeared in print the same year, is the original statement of what is now called the Church-Turing thesis.

History

Church's original system (1932-1933)

Alonzo Church, then at Princeton University, introduced lambda calculus in the early 1930s while pursuing two goals: clarifying the informal notion of "function" in mathematics, and constructing a logical system strong enough to serve as a foundation for mathematics. Church's earliest version appeared in "A Set of Postulates for the Foundation of Logic," Annals of Mathematics 33 (1932), with a continuation in 1933 [1]. At the end of the 1933 paper Church introduced an encoding for natural numbers in the untyped λ-calculus, allowing arithmetic to be carried out in a purely functional setting.

What was the Kleene-Rosser paradox?

Church's original system combined a logic of propositions with the lambda notation for functions, but it turned out to be inconsistent. In 1935 Stephen Kleene and J. Barkley Rosser, both Church's students, exhibited a paradox showing that the system could derive a contradiction in the style of Richard's antinomy (the Kleene-Rosser paradox) [6]. In response, Church separated the consistent computational core (the pure lambda calculus of abstraction, application, and conversion) from the surrounding logical apparatus. The pure calculus survived as a model of computation in its own right.

When did Church prove undecidability, and how does this relate to the Church-Turing thesis? (1936)

In April 1936 Church published "An Unsolvable Problem of Elementary Number Theory" in the American Journal of Mathematics, using lambda calculus to give the first proof that David Hilbert's Entscheidungsproblem (the decision problem of first-order logic) is unsolvable [2]. A follow-up note later that year in the Journal of Symbolic Logic gave the explicit application [3]. Independently, Alan Turing, then a graduate student at Cambridge, proved the same result in "On Computable Numbers, with an Application to the Entscheidungsproblem" (1936), introducing what we now call the Turing machine [7]. Turing later showed that the class of computable functions defined by his machines coincides with the class of λ-definable functions. The combined claim, that any effectively calculable function can be expressed in either formalism, became the Church-Turing thesis [18].

In the same year, Church and Rosser proved the confluence theorem now known as the Church-Rosser theorem: when reduction rules are applied to a λ-term, the order in which redexes are chosen does not affect the eventual result, so a term has at most one normal form.

The 1940 type system and the 1941 monograph

In 1940 Church published "A Formulation of the Simple Theory of Types" in the Journal of Symbolic Logic, attaching a type discipline to lambda calculus to recover a consistent logical system [4]. This is the first simply typed lambda calculus and remains the prototype for nearly all later typed functional languages. In 1941 Church collected the technical material on the untyped calculus in The Calculi of Lambda-Conversion (Princeton University Press, Annals of Mathematics Studies 6), a 77-page monograph that remained the standard reference for decades [5].

How did the lambda calculus lead to Lisp and functional programming? (1958-1980s)

In 1958 John McCarthy began work at MIT on a programming language for AI research, which became LISP. The 1960 Communications of the ACM paper "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I" described a small set of operators together with an anonymous-function notation borrowed from Church (the LAMBDA form) [8]. As later summaries put it, McCarthy showed that "with a few simple operators and a notation for anonymous functions borrowed from Church, one can build a Turing-complete language for algorithms." The lambda notation and the use of higher-order functions came directly from Church. Scheme, designed by Gerald Jay Sussman and Guy L. Steele at MIT in 1975, was the first Lisp dialect to support full lexical closure; their "Lambda Papers" (1975-1980) showed how lambda calculus could explain tail-call iteration and continuation-passing style [9].

Typed functional languages emerged from theorem proving. Robin Milner designed the original ML at Edinburgh from 1973 as the metalanguage of the LCF proof assistant; his 1978 paper introduced Hindley-Milner type inference. Standard ML was proposed in 1983 and codified in The Definition of Standard ML (1990). David Turner's Miranda was presented at FPCA 1985; the Haskell committee (formed at FPCA 1987) published Haskell 1.0 in April 1990 [19]. OCaml was released in 1996 by Xavier Leroy and colleagues at INRIA.

Type theory and proof assistants (1970s-present)

The period 1970-1990 saw a rapid expansion of typed lambda calculi. Jean-Yves Girard introduced the second-order polymorphic lambda calculus, now called System F, in his 1972 doctoral thesis [10]; John C. Reynolds rediscovered the same system in 1974 [11]. Per Martin-Löf developed intuitionistic type theory with dependent types in the 1970s and 1980s. Thierry Coquand introduced the Calculus of Constructions in his 1985 PhD thesis (Coquand and Gérard Huet, Information and Computation 76, 1988); it is the core of the Coq proof assistant [12]. In 1991 Henk Barendregt organized eight pure type systems into the now-standard lambda cube [13].

What does a lambda expression look like? (Syntax)

The untyped lambda calculus has only three syntactic constructs. Using a Backus-Naur form, an expression (or term) is given by:

e ::= x         (variable)
    | λx. e     (abstraction)
    | e1 e2     (application)

A variable x stands for an unknown value. An abstraction λx.M denotes the anonymous function whose parameter is x and whose body is M. An application M N means "apply the function M to the argument N." Application is left-associative, so M N P means (M N) P, and the body of an abstraction extends as far to the right as possible, so λx. M N means λx.(M N).

This tiny grammar suffices to encode any computable function. There are no built-in numbers, booleans, pairs, lists, conditionals, loops, or recursion; everything must be encoded using functions alone.

Free and bound variables

In an abstraction λx.M, the occurrence of x immediately after λ is a binder; the variable x is bound in M. Any occurrence of a variable not under such a binder is free. The set of free variables FV(M) is defined inductively: FV(x) = {x}, FV(λx.M) = FV(M) \ {x}, FV(M N) = FV(M) ∪ FV(N).

What is alpha equivalence?

The specific name of a bound variable does not matter: λx.x and λy.y both denote the identity function. Two terms that differ only in the consistent renaming of bound variables are called alpha-equivalent (α-equivalent), written M =α N. Alpha equivalence captures the intuition that "the particular choice of a bound variable, in an abstraction, does not (usually) matter," and it is treated as syntactic equality throughout the theory.

How does beta reduction work? (Reduction)

Computation in lambda calculus is performed by rewriting terms according to a small set of rules. Together these rules define the conversion relations of the calculus.

Alpha conversion

Alpha conversion is the renaming of a bound variable. Replacing the bound x in λx.M by some fresh variable y (with corresponding renaming of x throughout M) yields an alpha-equivalent term. Alpha conversion is needed before substitution to avoid accidentally capturing free variables.

Beta reduction

The central computation rule is beta reduction. A redex of the form (λx.M) N reduces in one step to the term obtained by substituting N for x in M, written M[x := N]:

(λx. M) N  →β  M[x := N]

The single-step relation →β generates a multi-step relation ↠β (its reflexive transitive closure) and an equivalence relation =β. Substitution must avoid variable capture: if a free variable in N would become bound after naive textual replacement, the offending bound variable in M is alpha-renamed to a fresh name first. Beta reduction is the engine of computation: evaluating a lambda program means repeatedly contracting redexes until no more remain.

Eta conversion

Eta conversion identifies a function with an abstraction that simply applies it to its argument:

λx. (M x)   ↔η  M     (provided x is not free in M)

Eta conversion expresses the principle of extensionality: two functions that produce the same result for every input are equal.

Normal forms and reduction strategies

A term is in normal form if no beta redex can be reduced inside it. A term that beta-reduces to a normal form is normalizing. Not every term has a normal form: the famous looping term Ω = (λx. x x)(λx. x x) reduces to itself in one beta step and never terminates.

The order in which redexes are chosen is called a reduction strategy. The major strategies are:

Strategy	Reduces first	Programming-language analogue	Property
Normal-order (leftmost-outermost)	Outermost-leftmost redex	Idealized lazy evaluation	Reaches a normal form whenever one exists
Applicative-order (leftmost-innermost)	Innermost-leftmost redex; arguments before functions	Call-by-value	May fail to terminate even when a normal form exists
Call-by-name	Outermost redex; arguments substituted unevaluated	Algol 60-style by-name parameters	Same termination guarantee as normal order; can repeat work
Call-by-need	Outermost redex; arguments evaluated at most once	Modern lazy evaluation as in Haskell	Same termination guarantee as call-by-name; avoids re-evaluation

Weak head normal form (WHNF) is a weaker notion: a term is in WHNF if its top-level structure is a variable, an abstraction, or an application of a variable. Lazy languages such as Haskell evaluate to WHNF rather than to full normal form.

Theorems

Church-Rosser theorem (confluence)

Proved by Church and Rosser in 1936, the Church-Rosser theorem states that beta reduction is confluent: if a term M reduces to both N1 and N2, then N1 and N2 in turn reduce to a common term P. As a corollary, every term has at most one normal form (up to alpha equivalence). The theorem justifies the phrase "the" normal form of a term and shows that, when reduction terminates, the answer does not depend on the chosen reduction order.

Standardization theorem

The standardization theorem (Curry and Feys, 1958) states that whenever M reduces to N, there is a standard reduction sequence from M to N, in which redexes are contracted in a fixed leftmost-outermost order. A consequence is that normal-order reduction reaches a normal form whenever one exists, even though applicative-order reduction might diverge.

Is beta-equivalence decidable?

The relation =β is undecidable: there is no algorithm that, given two arbitrary lambda terms M and N, decides whether M =β N [2]. This is the original undecidability result that Church established in his 1936 paper, and it is the lambda-calculus analogue of the unsolvability of the halting problem for Turing machines. Decidability of equivalence is recovered for the simply typed lambda calculus and other strongly normalizing systems.

What are Church encodings and Church numerals?

Because lambda calculus has no primitive data, all data structures are represented as functions. The standard encodings are due to Church.

Concept	Encoding	Example
Church numeral n	λf. λx. f^n x (the function that applies f to x exactly n times)	0 = λf.λx. x; 1 = λf.λx. f x; 2 = λf.λx. f (f x)
Successor	succ = λn.λf.λx. f (n f x)	succ 1 ↠β 2
Addition	plus = λm.λn.λf.λx. m f (n f x)
Boolean true	true = λa.λb. a (the projection onto the first argument)
Boolean false	false = λa.λb. b (projection onto the second argument)
Conditional	if c then t else e is encoded as c t e
Pair	pair = λa.λb.λs. s a b; fst = λp. p true; snd = λp. p false
List (Church)	nil and cons in the style of right folds; iteration through the list
Y combinator	Y = λf. (λx. f (x x)) (λx. f (x x))	Y g ↠β g (Y g), enabling general recursion

A Church numeral encodes the number n as the higher-order function that applies a given function f to an argument x exactly n times, so 0 = λf.λx. x and 2 = λf.λx. f (f x) [17]. Arithmetic then becomes function composition: addition, multiplication, and exponentiation are all definable as short lambda terms.

The Y combinator is a fixed-point combinator: for any function g, Y g is a fixed point of g, enabling recursive functions to be defined inside the calculus even though the syntax has no name-binding mechanism for self-reference. The Y combinator is attributed to Haskell Curry; Turing later (1937) gave a related fixed-point combinator Θ with a stronger reduction property.

Lambda calculus is equivalent in expressive power to SKI combinatory logic, a variable-free system based on the combinators S = λx.λy.λz. x z (y z), K = λx.λy. x, and I = λx. x. Every closed lambda term can be translated into an equivalent SKI term by bracket abstraction, and conversely. The equivalence makes combinatory logic a useful intermediate language for compilers of functional programs.

Typed lambda calculi

The untyped lambda calculus admits self-application, which makes it Turing-complete but also produces non-terminating terms (such as Ω above) without a normal form. Typed lambda calculi attach type information that rules out problematic self-application. The trade-off is computational power: the simply typed lambda calculus, for example, is strongly normalizing (every well-typed term has a normal form) and is no longer Turing-complete on its own.

System	Year and originator	Key feature	Notable use
Simply typed lambda calculus (λ→)	Church, 1940	Function types A → B over a set of base types	Foundation for typed functional languages
System F (polymorphic, second-order)	Girard 1972; Reynolds 1974 (independently)	Universal quantification over types: ∀α. A	Theoretical core of ML- and Haskell-style polymorphism
Fω	Girard, 1972	Adds type operators (functions from types to types)	Higher-kinded type systems
LF (Lambda Pi, λΠ)	Harper, Honsell, and Plotkin, 1987	Dependent function types Πx:A. B	Logical framework for encoding deductive systems
Calculus of Constructions (CoC)	Coquand 1985 (PhD thesis); Coquand and Huet 1988 (journal)	Combines polymorphism, type operators, and dependent types	Core of the Coq proof assistant
Calculus of Inductive Constructions (CIC)	Paulin-Mohring, 1989-1996	Adds inductive types to CoC	Implemented in Coq and (extended) in Lean

The lambda cube

Henk Barendregt's lambda cube, presented in "Introduction to Generalized Type Systems" (Journal of Functional Programming 1991), organizes eight typed lambda calculi as the vertices of a three-dimensional cube [13]. The three axes are the kinds of dependency permitted between terms and types:

Axis	Adds
Polymorphism	Terms depending on types (∀-quantification)
Type operators	Types depending on types
Dependent types	Types depending on terms

The vertex with no extensions is the simply typed calculus; the vertex with all three extensions is the Calculus of Constructions. The cube fits inside the still more general framework of pure type systems, in which a single uniform syntax can express all eight calculi by changing the table of allowed sorts.

What is the Curry-Howard correspondence?

The Curry-Howard correspondence is a structural isomorphism between formal proof systems and typed lambda calculi. The slogan is propositions as types, proofs as programs: each proposition corresponds to a type, each proof to a program of that type, and proof simplification to program evaluation [16].

The correspondence was discovered in stages. Curry observed in 1934 that the types of the basic combinators of combinatory logic match the axiom schemes of intuitionistic implicational logic. In 1969 William Alvin Howard circulated a manuscript (published 1980 in a Festschrift for Curry) showing that natural deduction for intuitionistic propositional logic corresponds precisely to the simply typed lambda calculus, with implication mapping to function types, conjunction to product types, and disjunction to sum types. Later work extended the correspondence to System F (the Girard-Reynolds isomorphism), to predicate logic and LF, and to higher-order logic and the Calculus of Constructions.

Writing a program in a sufficiently rich typed lambda calculus is therefore the same activity as writing a constructive proof. This is the basis of modern interactive proof assistants: Coq, Lean, Agda, and Idris are programming languages whose type systems can state and check arbitrary mathematical theorems.

How did the lambda calculus shape programming languages?

Lambda calculus is sometimes called the machine code of functional programming. The list below traces the languages most directly shaped by it.

Language	First release	Designer(s)	Lambda-calculus connection
Lisp	1958-1960	John McCarthy (MIT)	LAMBDA notation borrowed from Church
ML (original)	1973	Robin Milner (Edinburgh)	Metalanguage of the LCF prover; Hindley-Milner inference
Scheme	1975	Sussman and Steele (MIT)	First Lisp with full lexical closure
Standard ML	1983-1990	Milner, Tofte, Harper, MacQueen	Statically typed functional language; formal Definition (1990)
Miranda	1985	David Turner (Kent)	Pure, lazy, polymorphic; precursor to Haskell
Erlang	1986	Joe Armstrong et al. (Ericsson)	Functional core; influenced by Prolog and ML
Haskell	1990	Haskell committee	Lazy, pure, polymorphic; Hindley-Milner with type classes
OCaml	1996	Leroy et al. (INRIA)	ML-family with objects
Scala	2004	Martin Odersky (EPFL)	Functional + object-oriented on the JVM
F#	2005	Don Syme (Microsoft Research)	OCaml-derived language for .NET
Clojure	2007	Rich Hickey	Lisp dialect on the JVM with persistent data structures
Elm	2012	Evan Czaplicki	Pure functional language for browser front-ends

Beyond functional languages, lambda calculus has shaped nearly every modern mainstream language. JavaScript, Python, C++ (since C++11), Java (since version 8), Rust, Swift, C#, and Kotlin all support lambda expressions and closures, whose semantics is routinely explained using capture-avoiding substitution, lexical scope, and higher-order functions drawn from lambda calculus. The keyword lambda in Python and the λ-style anonymous function in many languages descend directly from Church's λ binder. The operation of partially applying a multi-argument function, called currying, takes its name from Haskell Curry, who popularized the technique first studied by Moses Schönfinkel in 1924.

Applications

Theoretical computer science

Lambda calculus is a canonical model of computation studied in computability theory and complexity theory. The equivalence of λ-definability with Turing computability and with Kleene's general recursive functions is the technical content of the Church-Turing thesis [18]. Many later models of computation (the pi-calculus, session types) extend lambda calculus rather than replacing it.

Programming-language semantics

Denotational and operational semantics of programming languages are routinely defined by translation into a typed lambda calculus. Dana Scott's domain theory provided the first mathematical models of the untyped lambda calculus in the late 1960s, and these models became the basis of denotational semantics. Plotkin's structural operational semantics uses small-step reduction rules in the spirit of beta reduction.

Type theory and proof assistants

The Calculus of (Inductive) Constructions and Martin-Löf type theory are the core formal systems of Coq, Lean, Agda, and Idris. Mathematical results verified in these systems include the Four Colour Theorem (Gonthier, 2005) and the Feit-Thompson Odd Order Theorem (Gonthier et al., 2012), both in Coq. The CompCert C compiler (Leroy, 2009) is a verified optimizing C compiler proved correct in Coq.

Compiler intermediate representations

Functional-language compilers commonly translate source programs into a typed lambda calculus, then perform optimizations on that intermediate representation before generating machine code. Continuation-passing style (CPS) and administrative normal form (ANF) are restricted lambda-calculus forms used as compiler IRs in Standard ML of New Jersey, the Glasgow Haskell Compiler (GHC), and OCaml. GHC in particular uses a typed intermediate language called Core, which is essentially a variant of System Fω with coercions.

Category theory

The simply typed lambda calculus with products is the internal language of cartesian closed categories (CCCs); types correspond to objects, terms to morphisms, and beta-eta equivalence to equality of morphisms. This connection, due to Lambek and Scott (1986), connects programming-language theory to category theory.

Why does the lambda calculus matter for AI?

Lambda calculus has been close to AI since the beginning of the field. McCarthy's Lisp (1958-1960) was the dominant language for AI research from the late 1950s into the 1990s [8]. Classical symbolic AI systems and the Lisp dialects used to build them (Maclisp, Interlisp, Common Lisp, Scheme) inherited the lambda notation and higher-order programming style directly from lambda calculus. The deep-learning era shifted most production AI work to Python and C++, but the lambda heritage is still visible: Python's lambda keyword for anonymous functions, the map/filter/reduce higher-order operators used throughout data pipelines, and the heavy use of function composition in array libraries all descend from this tradition. ("Lambda layers" in some neural-network frameworks, which wrap an arbitrary anonymous function as a model layer, are named after the same anonymous-function notion, though they are an engineering convenience rather than a use of the calculus itself.)

In modern AI research, the most important lambda-calculus connection runs through type theory and proof assistants. Dependently typed systems descended from the Calculus of Constructions are the standard tools for formalizing mathematics and software, and there is growing interest in using them to verify properties of machine-learning systems. Functional languages also play a role in AI infrastructure: Haskell appears in programming-language research, Scala underlies Apache Spark, and OCaml is widely used in compiler and verifier development. Program-synthesis systems such as DreamCoder learn programs in typed lambda calculi from examples, providing a point of contact between symbolic and statistical approaches to AI.

ELI5: Lambda calculus in plain terms

Imagine a language where the only thing you can do is make a tiny machine that takes one thing in and gives one thing out (that is a function), name the thing that goes in, and feed one machine into another. There are no numbers, no "if," no loops, and no built-in anything: just these little function-machines. The surprising fact is that this is enough to do every computation a normal computer can do. You can build numbers out of functions (a number is "do this action n times"), build true and false out of functions, and even build a machine that calls itself forever. Alonzo Church invented this game in the 1930s to study what "computing" really means, and decades later it became the secret blueprint behind functional programming languages and the keyword lambda you see in Python.

See also

References

Church, Alonzo. "A Set of Postulates for the Foundation of Logic." Annals of Mathematics 33 (1932): 346-366. https://www.jstor.org/stable/1968337
Church, Alonzo. "An Unsolvable Problem of Elementary Number Theory." American Journal of Mathematics 58, no. 2 (1936): 345-363. https://www.jstor.org/stable/2371045
Church, Alonzo. "A Note on the Entscheidungsproblem." Journal of Symbolic Logic 1, no. 1 (1936): 40-41. https://www.jstor.org/stable/2269326
Church, Alonzo. "A Formulation of the Simple Theory of Types." Journal of Symbolic Logic 5, no. 2 (1940): 56-68. https://www.jstor.org/stable/2266170
Church, Alonzo. The Calculi of Lambda-Conversion. Annals of Mathematics Studies 6. Princeton University Press, 1941. https://archive.org/details/AnnalsOfMathematicalStudies6ChurchAlonzoTheCalculiOfLambdaConversionPrincetonUniversityPress1941
Kleene, Stephen C., and J. Barkley Rosser. "The Inconsistency of Certain Formal Logics." Annals of Mathematics 36, no. 3 (1935): 630-636. https://www.jstor.org/stable/1968646
Turing, Alan M. "On Computable Numbers, with an Application to the Entscheidungsproblem." Proceedings of the London Mathematical Society, series 2, 42 (1936-37): 230-265. https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
McCarthy, John. "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I." Communications of the ACM 3, no. 4 (1960): 184-195. https://www.cs.tufts.edu/~nr/cs257/archive/john-mccarthy/recursive.pdf
Sussman, Gerald J., and Guy L. Steele. "Scheme: An Interpreter for Extended Lambda Calculus." MIT AI Memo 349, December 1975. https://dspace.mit.edu/handle/1721.1/5794
Girard, Jean-Yves. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse d'État, Université Paris VII, 1972.
Reynolds, John C. "Towards a Theory of Type Structure." In Programming Symposium, Lecture Notes in Computer Science 19, 408-425. Springer, 1974. https://link.springer.com/chapter/10.1007/3-540-06859-7_148
Coquand, Thierry, and Gérard Huet. "The Calculus of Constructions." Information and Computation 76, nos. 2-3 (1988): 95-120. https://www.sciencedirect.com/science/article/pii/0890540188900053
Barendregt, Henk. "Introduction to Generalized Type Systems." Journal of Functional Programming 1, no. 2 (1991): 125-154. https://homepages.inf.ed.ac.uk/wadler/papers/barendregt/pure-type-systems.pdf
Barendregt, Henk. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic 103. North-Holland, 1984 (revised 1985). https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/103
Pierce, Benjamin C. Types and Programming Languages. MIT Press, 2002. https://mitpress.mit.edu/9780262162098/types-and-programming-languages/
Wadler, Philip. "Propositions as Types." Communications of the ACM 58, no. 12 (2015): 75-84. https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
Alama, Jesse, and Johannes Korbmacher. "The Lambda Calculus." Stanford Encyclopedia of Philosophy. Stanford University, 2018. https://plato.stanford.edu/entries/lambda-calculus/
Copeland, B. Jack. "The Church-Turing Thesis." Stanford Encyclopedia of Philosophy. Stanford University, revised 2024. https://plato.stanford.edu/entries/church-turing/
Hudak, Hughes, Peyton Jones, and Wadler. "A History of Haskell: Being Lazy with Class." HOPL III (2007). https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/history.pdf
Cardone, Felice, and J. Roger Hindley. "Lambda-Calculus and Combinators in the 20th Century." In Handbook of the History of Logic, vol. 5. Elsevier, 2009.
McCarthy, John, et al. LISP 1.5 Programmer's Manual. MIT Press, 1962. https://www.softwarepreservation.org/projects/LISP/book/LISP%201.5%20Programmers%20Manual.pdf

Editing: Lambda Calculus