Typ-Prüfung bei Funktions-Aufrufen

• (einstellig)

  wenn f : : A₁$\to$B und X₁ : : A₁,

  dann f (X₁) : : B

• (zweistellig)

  wenn f : : A₁×A₂$\to$B und X₁ : : A₁ und X₂ : : A₂,

  dann f (X₁, X₂) : : B

• (entspr. für andere Stelligkeiten)

Analogie zur Aussagenlogik:

wenn A₁$\to$B und A₁ wahr ist, dann ist B wahr.

(Curry-Howard-Isomorphie, Calculus of Constructions)