Unsolvability of type correctness problem for functional programs

В работе рассматривается проблема типовой корректности функциональных программ, не содержащих информацию о типах переменных. Цель данного исследования – доказать несуществование такого алгоритма, который отверг бы все программы, во время исполнения которых происходит ошибка типа, и принял бы все программы, во время исполнения которых ошибки типа не происходит.