# Lambda Calculus

> Source: https://aiwiki.ai/wiki/lambda_calculus
> Updated: 2026-06-25
> Categories: Computer Science, Mathematics, Programming Languages
> From AI Wiki (https://aiwiki.ai), a free encyclopedia of artificial intelligence. Quote with attribution.

**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](/wiki/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](/wiki/church_turing_thesis) [18].

Lambda calculus is the theoretical foundation of [functional programming](/wiki/functional_programming). Its concepts of higher-order functions, substitution, and reduction directly inspired [LISP](/wiki/lisp) (designed by [John McCarthy](/wiki/john_mccarthy) in 1958, published in 1960) [8] and the family of statically typed functional languages including [ML](/wiki/ml_programming_language), [OCaml](/wiki/ocaml), and [Haskell](/wiki/haskell). Its typed variants, from the simply typed lambda calculus through dependently typed systems, form the basis of modern [type theory](/wiki/type_theory) and the [proof assistants](/wiki/proof_assistant) 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](/wiki/computability_theory) 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](/wiki/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](/wiki/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](/wiki/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](/wiki/dependent_type) 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](/wiki/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](/wiki/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](/wiki/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](/wiki/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](/wiki/coq), [Lean](/wiki/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](/wiki/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](/wiki/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

- [Lisp](/wiki/lisp)
- [Scheme](/wiki/scheme)
- [Alonzo Church](/wiki/alonzo_church)
- [Alan Turing](/wiki/alan_turing)
- [Church-Turing thesis](/wiki/church_turing_thesis)
- [Turing machine](/wiki/turing_machine)
- [Functional programming](/wiki/functional_programming)
- [Combinatory logic](/wiki/combinatory_logic)
- [Currying](/wiki/currying)
- [Type theory](/wiki/type_theory)
- [Lean (theorem prover)](/wiki/lean)
- [John McCarthy](/wiki/john_mccarthy)

## References

1. Church, Alonzo. "A Set of Postulates for the Foundation of Logic." *Annals of Mathematics* 33 (1932): 346-366. https://www.jstor.org/stable/1968337
2. 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
3. Church, Alonzo. "A Note on the Entscheidungsproblem." *Journal of Symbolic Logic* 1, no. 1 (1936): 40-41. https://www.jstor.org/stable/2269326
4. 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
5. Church, Alonzo. *The Calculi of Lambda-Conversion*. Annals of Mathematics Studies 6. Princeton University Press, 1941. https://archive.org/details/AnnalsOfMathematicalStudies6ChurchAlonzoTheCalculiOfLambdaConversionPrincetonUniversityPress1941
6. 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
7. 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
8. 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
9. 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
10. 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.
11. 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
12. 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
13. 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
14. 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
15. Pierce, Benjamin C. *Types and Programming Languages*. MIT Press, 2002. https://mitpress.mit.edu/9780262162098/types-and-programming-languages/
16. 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
17. Alama, Jesse, and Johannes Korbmacher. "The Lambda Calculus." *Stanford Encyclopedia of Philosophy*. Stanford University, 2018. https://plato.stanford.edu/entries/lambda-calculus/
18. Copeland, B. Jack. "The Church-Turing Thesis." *Stanford Encyclopedia of Philosophy*. Stanford University, revised 2024. https://plato.stanford.edu/entries/church-turing/
19. 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
20. 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.
21. 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