From 9f600fc0c3d6ffabbe9ad9b4423021705dd5728c Mon Sep 17 00:00:00 2001 From: TurtlePU Date: Mon, 7 Oct 2024 06:17:17 +0300 Subject: [PATCH] + DependoBuf, Twelf projects --- docs/projects/dependobuf.md | 29 +++++++++++++++++++++++++++++ docs/projects/twelf.md | 14 ++++++++++++++ mkdocs.yml | 8 ++++---- 3 files changed, 47 insertions(+), 4 deletions(-) diff --git a/docs/projects/dependobuf.md b/docs/projects/dependobuf.md index 71b05f5..9047102 100644 --- a/docs/projects/dependobuf.md +++ b/docs/projects/dependobuf.md @@ -5,3 +5,32 @@ tags: --- # Протокол для сериализации структурированных данных с зависимыми типами + +## Описание + +[DependoBuf](https://github.com/SphericalPotatoInVacuum/DependoBuf) — +очередной протокол для сериализации структурированных данных. Однако в отличие +от [ProtoBuf](https://protobuf.dev) и иже подобным, наш протокол позволяет +описание более сложных структур данных: сбалансированных деревьев, массивов +фиксированной длины, матриц, особым образом провалидированных данных... + +Всё это возможно благодаря особенной системе типов, включающей в себя зависимые +типы таким образом, чтобы сохранять разрешимость проверки типов (т.е. в отличие +от C++, для DependoBuf существует алгоритм, за конечное время проверяющий +корректность составленной программы). + +В ходе предшествующей работы над проектом, в DependoBuf была реализована +собственно процедура проверки типов, протокол (де)сериализации в/из байтовых +последовательностей, а также кодогенерация в различные мейнстримные языки +программирования. + +В этом году предлагается завершить основной этап работы над проектом, + +1. убедившись в совместимости различных алгоритмов кодогенерации; +2. переписав проект с C++ на Rust; +3. дописав в кодогенерации методы для (де)сериализации типов данных. + +## База данных для типов данных DependoBuf + +Кроме этого, интересной задачкой является реализация базы данных, поддерживающей +хранение данных, схема которых описана в протоколе. diff --git a/docs/projects/twelf.md b/docs/projects/twelf.md index 1aa9fad..141456f 100644 --- a/docs/projects/twelf.md +++ b/docs/projects/twelf.md @@ -5,3 +5,17 @@ tags: --- # Языковой сервер для Twelf + +[Twelf](https://twelf.org) — крайне интересный язык программирования, +особенный тем, что в нём есть зависимые типы (типы, зависящие от значений), +но нет правил редукции (вычисления термов). Получается крайне интересная +система, в которой, помимо всего прочего, легко кодировать грамматики языков +программирования. Благодаря этому, Twelf часто используется для формализации +доказательств свойств логических систем (коими языки программирования, конечно +же, являются). + +Однако серьёзным недостатком Twelf является отличие сколько-нибудь комфортного +тулинга — рекомендуемым способом программирования на Twelf является +программирование в консоли. В данной дипломной работе предлагается исправить +столь зияющий недостаток и реализовать языковой сервер (и плагин для VS Code) +для Twelf для упрощения разработки на нём. diff --git a/mkdocs.yml b/mkdocs.yml index 60c0239..6708e40 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -5,18 +5,18 @@ nav: - Главная: index.md - Проекты: - projects/index.md - - projects/catcomp.md + - projects/sanskrit.md + - projects/zksnark.md - projects/codeaswiki.md - projects/dependobuf.md + - projects/twelf.md + - projects/catcomp.md - projects/gc.md - projects/graphcat.md - projects/hitgc.md - projects/mlgc.md - projects/parsergen.md - - projects/sanskrit.md - projects/shaderdsl.md - - projects/twelf.md - - projects/zksnark.md - testtask.md theme: name: material