Перейти к содержанию

Языковой сервер для Twelf

Twelf — крайне интересный язык программирования, особенный тем, что в нём есть зависимые типы (типы, зависящие от значений), но нет правил редукции (вычисления термов). Получается крайне интересная система, в которой, помимо всего прочего, легко кодировать грамматики языков программирования. Благодаря этому, Twelf часто используется для формализации доказательств свойств логических систем (коими языки программирования, конечно же, являются).

Однако серьёзным недостатком Twelf является отличие сколько-нибудь комфортного тулинга — рекомендуемым способом программирования на Twelf является программирование в консоли. В данной дипломной работе предлагается исправить столь зияющий недостаток и реализовать языковой сервер (и плагин для VS Code) для Twelf для упрощения разработки на нём.