Семантика языка предикатного программирования P формализована с использованием трех видов отношений: совместимости, согласованности и тождества. Рекурсивные типы определены через аппарат наименьшей неподвижной точки. Обобщенные типы представлены типовыми ограничениями (концептами). Для конструкций с неявной типизацией сформулированы правила восстановления типов переменных. Разработаны алгоритмы проверки корректности рекурсии, определения типов для языковых конструкций, проверки семантической корректности конструкций.