section_heading: Logika
paragraph_text: Curry-Howard izomorfizam implicira vezu između logike i programiranja: svaki dokaz teorema intuicionističke logike odgovara redukciji tipiziranog lambda termina, kao i obratno. Štoviše, teoremi se mogu identificirati signaturama tipa funkcije. Specifično, tipizirana kombinatorna logika odgovara Hilbertovom formalnom sustavu (koji se sastoji od aksioma i pravila inferencije) u teoriji dokaza.