Calculus of constructions (CoC)

Layer 0 — Mathematicsin the proof-theory subtree

Coquand-Huet 1988: dependently-typed λ-calculus extending System F + Martin-Löf. Foundation of Coq. Bridges proof-theory + type-theory + programming-languages.