Лабораторія «Групоїд Інфініті»
Лабораторія «Групоїд Інфініті» інституту формальної математики курує низку мов програмування для математиків. Процес роботи лабораторії, а також перелік мов програмування описаний на сторінці головного артефакту лабораторії — методології верифікації теорем AXIO/1.
Головні наукові напрямки лабораторії: диференціальна геометрія, алгебраїчна топологія, супергеометрія, стабільна хроматична теорія гомотопій, сімпліціальна теорія, К-теорія з точки зору теорії типів.
Принципи лабораторії:
- Експліцитна типізація — чітке визначення типів для забезпечення швидкості, надійності та прозорості;
- Мінімальні ядра — дослідження компактних і ефективних базових конструкцій;
- Підтримка сильних властивостей — гарантія математичної коректності й строгих інваріантів;
- Фокусування на швидкості тайпчекінгу — оптимізація процесів перевірки типів для практичної застосовності;
- Педагогічність і лаконічність — створення інтуїтивно зрозумілих і стислих інструментів для навчання та досліджень;
- Модульність і композиційність — розробка систем, які легко розширюються та комбінуються;
- Формальна верифікація — акцент на доведенні коректності програм і математичних конструкцій;
- Універсальність абстракцій — створення гнучких інструментів, придатних для широкого спектра математичних задач.
