Объясняю: математики заметили связь между программами и математическими доказательствами (тут читаем про изоморфизм Карри-Говарда). Так вот исчисление предикатов соответствует лямбда-исчислению с зависимыми типами.
Это объяснение на пальцах.
Подробнее читаем в учебнике Пирса «Типы в языках программирования».
