Типизация и организация контроля типов в программах над сложными структурами данных

Предлагаются средства спецификации программ с помощью логических формул. Рассматривается метод организации типового контроля при заданной таким образом спецификации.