Izomorfizm Curry’ego-Howarda

Izomorfizm Curry’ego-Howarda – określenie odpowiedniości pomiędzy termami rachunku lambda z typami a dowodami logiki intuicjonistycznej. Odpowiedniość ta pozwala na wyrażanie dowodów twierdzeń jako funkcji, co stało się podstawą dla licznych systemów dowodzenia twierdzeń opartych na logice intuicjonistycznej, takich, jak np. Coq.

Linki zewnętrzne

• Lambda Calculi With Types - artykuł Henka Barendregta omawiający rachunki lambda z typami i odpowiadające im systemy logiczne.