Logic of constructions. ⊥ has no proof. Proof of X∧Y is a pair (pX,pY). Proof of X∨Y is a tagged value (e.g., pair ⟨0,pX⟩ or ⟨1,pY⟩). ∀ and → are functions/constructions transforming proofs. Foundation for Type Theory.