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[1].
Przypisy
- ↑ Welcome! | The Coq Proof Assistant [online], coq.inria.fr [dostęp 2017-11-24] (ang.).
Linki zewnętrzne
- Lambda Calculi With Types - artykuł Henka Barendregta omawiający rachunki lambda z typami i odpowiadające im systemy logiczne.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.