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

Это объяснение на пальцах.

Подробнее читаем в учебнике Пирса «Типы в языках программирования».