Категорные модели линейной теории типов с субэкпоненциальными модальностями (продолжение)

Субэкспоненциалы являются естественным обобщением экспоненциального оператора из линейной логики. Если экспоненциал ограниченно вводит правила сокращения и ослабления, тогда как субэкспоненциал, в общем случае, — это модальный оператор, чьи формальные свойства напоминают оператор $\Box$ в логике S4, который либо вводит правило ослабления (аффинный субэкспоненциал), либо правило сокращения (релевантный субэкспоненциал), либо оба, либо ни одного. В литературе ранее изучались полимодальные обобщения линейной логики с субэкспоненциалами в контексте теории доказательств и конкретных применений в прикладной информатике, но семантический анализ был проведен довольно ограниченно. В этом докладе, мы введем теоретико-типовую версию интуиционисткой линейной логики с субэкспоненциалами и кратко обсудим её теоретико-доказательные аспекты, в частности, нормализацию выводов. Далее мы введем ряд понятий, позволяющих ввести адекватную денотационную семантику, основанную на симметрических моноидальных замкнутых категорий, снабженных семейством комонад определенного рода и естественных преобразований между ними. Далее, мы дадим обобщение ряда результатов из 1990-х годов и покажем, как модели таких систем типов эквивалентно характеризуются как так называемые моноидальные сопряжения. В частности, мы покажем как осуществить такую характеризацию 2-категории всех моделей как полной 1,2-подкатегории 2-категории 2-функторов определенного вида. По возможности, автор постарается дать пропедевтическое введение в необходимые понятия и факты из теории 2-категорий и формальной теории комонад.