# References & further reading

A curated, tiered reading list for the whole course. The bibliography below is generated from
[`references.bib`](https://github.com/nasqret/vietnam2026/blob/main/book/references.bib).

## Core

- **Sørensen & Urzyczyn**, *Lectures on the Curry–Howard Isomorphism* — the spine of Lectures 1–3.
- **Barendregt**, *The Lambda Calculus* — the reference for Lecture 2.
- **Riehl**, *A Reintroduction to Proofs* (Lean game) — the backbone of Lecture 3.
- **Macbeth**, *The Mechanics of Proof* & the **Natural Number Game** — Lecture 4.
- **Mathlib** documentation and the **Lean** community pages — Lectures 4–6.

## Supplementary

- **Girard, Lafont & Taylor**, *Proofs and Types*.
- **Pierce**, *Types and Programming Languages*.
- **Nederpelt & Geuvers**, *Type Theory and Formal Proof*.
- **Avigad**, *Mathematical Logic and Computation*.

## Advanced / foundations

- **Martin-Löf**, *Intuitionistic Type Theory*.
- **The Univalent Foundations Program**, *Homotopy Type Theory*.
- **Church** (1936, 1940) and **Howard** (1980) — the primary sources.

## Capstone

- **Odrzywołek**, *All elementary functions from a single binary operator* (arXiv:2603.21852), with its
  [Lean 4 formalization](https://github.com/nasqret/eml-formalization).

---

## Full bibliography

```{bibliography}
:all:
```