Curryho–Howardův isomorfismus

Curryho–Howardův isomorfismus je v logice a teorii typů rovnocennost mezi typy a formulemi, resp. jejich důkazy. Logickým objektům (konektivům a konstantám) odpovídají typy takto:

Výroková logika	Teorie typů
implikace	funkční typ
konjunkce	součinový typ
disjunkce	součtový typ
pravda	jednotkový typ
nepravda	prázdný typ

Kvantifikátory v logice prvního řádu odpovídají závislostním typům:

Predikátová logika	Teorie typů
${\displaystyle \forall }$	zobecněný součinový typ
${\displaystyle \exists }$	zobecněný součtový typ

Pro rovnost se používá zvláštní typ ${\displaystyle a=_{A}b}$, jehož jedinou hodnotou je Refl.^[1]

Konkrétní hodnoty jednotlivých typů přímo odpovídají důkazům formulí.