09-29-2026, 11:41 PM
Proofs and Types by Jean-Yves Girard, translated and supplemented by Paul Taylor and Yves Lafont, is a foundational introduction to the relationship between logic, proof theory, type theory, and computer science. Originally developed from graduate lectures on typed $\lambda$-calculus, the book develops the idea that a logical proposition can be viewed as a type, while a proof can be regarded as a program or term inhabiting that type. This perspective is the basis of the Curry–Howard correspondence, which connects mathematical proofs with computation.
The book begins by distinguishing syntax and proofs from semantics and denotation, and then develops natural deduction from a constructive viewpoint. Under this interpretation, logical connectives acquire computational meanings: a proof of $A \land B$ contains proofs of both $A$ and $B$, a proof of $A \Rightarrow B$ is a function transforming proofs of $A$ into proofs of $B$, and existential and universal quantifiers receive analogous computational interpretations. This leads naturally to the $\lambda$-calculus, where propositions become types and proofs become typed terms. For example, a function of type $A \to B$ represents a constructive method for transforming an object of type $A$ into one of type $B$.
A central theme is normalization and computation. Logical deductions can be transformed by eliminating unnecessary intermediate steps, while $\lambda$-terms can be reduced through computational rules. Thus, proof normalization and program evaluation are closely related processes. The book then extends the basic typed $\lambda$-calculus to more expressive systems, including Gödel's System T, with natural numbers, recursion, and booleans, and System F, which introduces polymorphism and second-order types. These systems demonstrate how increasingly sophisticated mathematical constructions can be represented computationally.
The later chapters move toward sequent calculus, cut elimination, second-order logic, polymorphism, semantics, and linear logic. Girard's linear logic changes the treatment of assumptions by making the use of resources explicit: propositions are not simply reusable indefinitely, which gives the logic a strong connection with resource-sensitive computation. The appendices further discuss semantics of System F, coherence spaces, domains, and the interpretation of types and terms. Overall, the book presents a unified view in which logic can be understood computationally: proving a proposition, constructing a typed program, and performing a computation are different manifestations of closely related structures.
Key takeaways
BOOK [PDF]
The book begins by distinguishing syntax and proofs from semantics and denotation, and then develops natural deduction from a constructive viewpoint. Under this interpretation, logical connectives acquire computational meanings: a proof of $A \land B$ contains proofs of both $A$ and $B$, a proof of $A \Rightarrow B$ is a function transforming proofs of $A$ into proofs of $B$, and existential and universal quantifiers receive analogous computational interpretations. This leads naturally to the $\lambda$-calculus, where propositions become types and proofs become typed terms. For example, a function of type $A \to B$ represents a constructive method for transforming an object of type $A$ into one of type $B$.
A central theme is normalization and computation. Logical deductions can be transformed by eliminating unnecessary intermediate steps, while $\lambda$-terms can be reduced through computational rules. Thus, proof normalization and program evaluation are closely related processes. The book then extends the basic typed $\lambda$-calculus to more expressive systems, including Gödel's System T, with natural numbers, recursion, and booleans, and System F, which introduces polymorphism and second-order types. These systems demonstrate how increasingly sophisticated mathematical constructions can be represented computationally.
The later chapters move toward sequent calculus, cut elimination, second-order logic, polymorphism, semantics, and linear logic. Girard's linear logic changes the treatment of assumptions by making the use of resources explicit: propositions are not simply reusable indefinitely, which gives the logic a strong connection with resource-sensitive computation. The appendices further discuss semantics of System F, coherence spaces, domains, and the interpretation of types and terms. Overall, the book presents a unified view in which logic can be understood computationally: proving a proposition, constructing a typed program, and performing a computation are different manifestations of closely related structures.
Key takeaways
- Curry–Howard correspondence: propositions correspond to types, and proofs correspond to programs/terms.
- Constructive logic: a proof carries computational information, rather than merely establishing truth.
- $\lambda$-calculus: provides the fundamental computational language underlying typed proofs.
- Proof normalization: simplifying a proof corresponds closely to evaluating a program.
- Function types: a proof of $A \Rightarrow B$ can be interpreted as a function from proofs of $A$ to proofs of $B$.
- System T: demonstrates how recursion and arithmetic can be incorporated into typed computation.
- System F: introduces polymorphism and substantially increases the expressive power of the type system.
- Sequent calculus and cut elimination: provide important proof-theoretic mechanisms for understanding the structure and computation of proofs.
- Linear logic: treats assumptions as resources, creating a closer connection between logic and resource-sensitive computation.
- Main philosophical idea: proof theory, programming languages, and computation are deeply interconnected, rather than being separate disciplines.
BOOK [PDF]
┌────────────────────────────────┐
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘