Исследовательская группа

Лаборатория языковых инструментов

"Жидкие" типы

September 18

В докладе будет дано описание "Жидких типов" (Liquid types - Logically Qualified Data Types), а также представлен алгоритм вывода этих типов для языка ML. Liquid types - это особый вид зависимых типов, в котором тип выражения может быть "уточнен" с помощью предиката в некоторой разрешимой логике. Алгоритм вывода жидких типов основан на алгоритме Хиндли-Милнера и методе абстрактной интерпретации под названием Predicate abstraction. На практике liquid types могут быть использованы для верификации широкого класса программ, например для статической проверки выхода за границы массива.

Материалы к докладу: http://goto.ucsd.edu/~rjhala/liquid/liquid_types.p...

Докладчик: Евгений Моисеенко