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.
Przypisy
Linki zewnętrzne Lambda Calculi With Types - artykuł Henka Barendregta omawiający rachunki lambda z typami i odpowiadające im systemy logiczne.
Kategoria:Logika matematyczna