[Семинар в Беркли] Эван Паттерсон (Институт Топос) | Единая теория типов для внутренних языков

Название: Единая теория типов для внутренних языков субструктурных категориальных логик Аннотация: Внутренний язык категориальной структуры, являющийся связующим звеном между теорией категорий и теорией типов, позволяет задавать морфизмы в эргономичной нотации, основанной на элементах и применении функций. Поиск внутреннего языка обычно представляет собой ручной процесс, выполняемый заново для каждой категориальной структуры. Мы предлагаем единую теорию типов, предоставляющую внутренние языки для множества различных категориальных структур, соответствующих субструктурным логикам, некоторые из которых хорошо известны, а другие — менее. Рассматриваемые структуры включают категории, мультикатегории (планарные, симметричные и декартовы), PROP, теории Ловера, (симметричные) моноидальные категории, декартовы категории, категории Маркова и категориальные понятия схем баз данных. Мы представляем основные идеи и избранные примеры этой теории типов, а также представляем предварительную реализацию теории типов, разработанную нашим коллегой tslil clingman. Дата: 29 сентября 2026 г. Ссылка на слайды: https://www.epatters.org/assets/slides/2026-09-berkeley-seminar/slides.html