Curry-Howard correspondence

Layer 0 — Mathematicsin the proof-theory subtree

Curry 1958 / Howard 1969: types ≡ propositions, programs ≡ proofs, evaluation ≡ proof-normalisation. Cross-listed with L0 logic. Foundation of dependent-type-theory + proof-assistants.