Covalue

Следующая лекция по теориям типов (STLC и System T) пройдет в среду 5 августа, в то же время (19:00 CEST/UTC+2 / 20:00 MSK).

Онлайн-курс «Современные теории типов» В среду 15 июля в 19:00 CEST/UTC+2 (20:00 MSK) в Лаборатории формальной математики стартует курс по современным теориям типов. Лекции читают @akuklev и @clayrat по средам, примерно по часу, частота - раз в неделю (с…

Онлайн-курс «Современные теории типов» В среду 15 июля в 19:00 CEST/UTC+2 (20:00 MSK) в Лаборатории формальной математики стартует курс по современным теориям типов. Лекции читают @akuklev и @clayrat по средам, примерно по часу, частота - раз в неделю (с летними пропусками). Начнём с обзора формальных языков и алгебраических теорий и пойдём до самого фронтира синтетических и направленных теорий типов. Примерная программа: 1. Вводная лекция 2. Языки и алгебраические теории 3. STLC и System T 4. PCF 5. System F и Fω 6. Зависимо-типизированные языки 7. Индукция 8. Рефайнмент- и фактор-типы 9. Эффекты в типах 10. HoTT 11. OTT/CuTT 12. □-полиморфизм 13. Модальные типы 14. Охраняемая рекурсия 15. Когезивные модальности 16. Направленные и симплициальные теории Не требуется предварительной подготовки по теории типов, но пригодятся базовые познания в функциональном программировании и алгебре. Знание теории категорий для понимания курса в целом не нужно, за одним исключением: мы будем обсуждать внутренние языки категорий и топосов (определение топоса дадим по ходу), где не помешает помнить определение декартово замкнутой категории. Ссылка на гугл-календарь, где будем публиковать даты лекций: https://calendar.google.com/calendar/u/0?cid=YzdkMGI0MTdlZjFiMTg1OGVmNzUyYjFkZjBjYjYwZjBhYTI0MGExNjlhMWVhZGY5OTcyOGYwOTM4OTVlMDliM0Bncm91cC5jYWxlbmRhci5nb29nbGUuY29t

Сегодня в 12:30 UTC (через ~2 часа) планирую постримить формализацию понятия рефлексивных графов.

Сегодня в 12:30 UTC (через ~2 часа) планирую постримить формализацию понятия рефлексивных графов.

Сегодня в 12:45 UTC (через ~2.5 часа) планирую постримить на ютюб-канале формализацию Symmetry Book на кубических типах.

Сегодня в 12:45 UTC (через ~2.5 часа) планирую постримить на ютюб-канале формализацию Symmetry Book на кубических типах.

Формализация краткого вывода закона исключенного третьего из аксиомы выбора (узнал от Валерия Исаева): https://gist.github.com/clayrat/80f2e048831e6829a49d5cb3843b2c7d

Сегодня в 12:00 UTC (через ~1.5 часа) планирую постримить разбор PoC компилятора в пучки.

Сегодня в 12:00 UTC (через ~1.5 часа) планирую постримить разбор PoC компилятора в пучки.

Сегодня в 12:00 UTC (через 2.5 часа) планирую постримить разбор статьи о программировании на полиномиальных функторах.

Сегодня в 12:00 UTC (через 2.5 часа) планирую постримить разбор статьи о программировании на полиномиальных функторах.

Сегодня в 12:30 UTC (через 1.5 часа) планирую постримить на ютюб-канале разбор диалоговой семантики и вайб-кодинг солвера на её основе. Подключайтесь, кому интересно!

Сегодня в 12:30 UTC (через 1.5 часа) планирую постримить на ютюб-канале разбор диалоговой семантики и вайб-кодинг солвера на её основе. Подключайтесь, кому интересно!

Grandury, Nanevski, Gryzlov, [2025] "Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach" В прошлом августе у нас наконец-то вышла статья, идею которой я предложил где-то в 2022 году и периодически возился с её имплементацией. В самой статье основная идея в явном виде не выписана, но суть там вот в чём. В теории типов наиболее общим представлением ориентированного графа обычно полагается функция A → A → U, где A — тип вершин графа, а U — вселенная («тип типов»), то есть гомогенный бинарный предикат. Используя классическую эквивалентность (см. например HoTT book, 4.8.3) ∑[T:U] (T → A) ≃ (A → U), мы можем трансформировать определение графа в пару { edge : A → U, adj : (from : A) → edge from → A }, то есть в представление в виде adjacency map, которое сопоставляет исходным вершинам рёберные конструкции и умеет по ним извлекать конечную вершину. Специализируя эту конструкцию под конечные графы и структуры данных, мы получаем из неё классические представления adjacency matrix/list. Идея, лежащая в основе статьи, заключается в том, что такое представление удобно и для работы на логическом уровне, по крайней мере, для алгоритмов, работающих как поиск в глубину, то есть стартующих из одной вершины, и транзитивно проходящих по всем исходящим из неё ребрам. В частности, раз мы можем запихнуть орграф в конечное отображение, его можно использовать как частичный коммутативный моноид (Partial Commutative Monoid, PCM) в сепарационной логике. (Частичная) операция моноида - дизъюнктное объединение отображений с непересекающимися областями определения. Чтобы она заработала, достаточно договориться, что графы могут быть частичными, то есть допускать висячие ребра, где исходная вершина лежит в нужном подграфе, а конечная уже за его пределами. При объединении висячие ребра могут склеиваться в обычные ребра, находя свои конечные вершины. В классической сепарационной логике рассматривается в первую очередь PCM куч (heaps). Как только у нас появился второй PCM, мы можем рассмотреть отображения (морфизмы) между ними, а также эндоморфизмы над самими графами. Морфизм в данном случае это функция, сохраняющая моноидальную операцию, f(γ₁∙γ₂) = fγ₁∙fγ₂. Это позволяет распространить концепцию фрейминга (framing) на графы - в статье мы называем это "контекстной локализацией" (contextual localization). Другими словами, морфизмы позволяют вычленить кусок графа, произвести над ним некоторое действие, и затем автоматически склеить его с незатронутой оставшейся частью, что сильно упрощает ряд доказательств. Морфизмами, в частности, являются высокоуровневые комбинаторы над кодировкой графов как конечных отображений - map, filter, а также более ad-hoc функции вроде взятия множеств конечных вершин sinks. Достижимость (reachability) в графе сама по себе морфизмом не является, но удобно взаимодействует с морфизмом filter, что позволяет "вырезать" фрагменты из достижимых компонент. Весь этот аппарат мы используем для создания библиотеки работы с графами в Hoare Type Theory, и построения двух формальных доказательств для императивных алгоритмов Шорра-Уэйта (разметка бинарного графа, где стек обхода хранится в самом графе через инверсию рёбер, без выделения отдельной памяти) и union-find (построение непересекающихся классов эквивалентности). Доказательства получились достаточно компактными (110 строк для Шорра-Уэйта, 49 для union-find). Ограничение описанной техники вытекает из исходной идеи - она естественна для алгоритмов, исследующих граф, следуя по ребрам. Для алгоритмов, работающих с ребрами более "глобально" (например, алгоритм Краскала), скорее всего, потребуются другие представления. #paper #separationlogic

Выложили запись доклада: https://www.youtube.com/watch?v=IkTimIZUCgg

Piecha, [2013] "Three Lectures on Dialogues" Три лекции по диалоговой семантике интуиционистской логики. Диалоговая семантика - это интерпретация логических формул, придуманная Паулем Лоренценом и его учеником Куно Лоренцем в 1950х годах. Она основана на идее игры между игроком и оппонентом, где валидность формулы определяется как наличие у игрока выигрышной стратегии при любом поведении оппонента. Фактически, это предшественник игровой семантики. Лекции устроены так: 1. Введение в диалоги Лоренцена для пропозициональной логики: формулы, атаки/защиты, позиции, D-диалоги, стратегии, полнота, классические обобщения. 2. Расширение пропозициональной логики на Хорновские дизъюнкты в стиле логического программирования: E-диалоги, прологовский дефинициональный ризонинг (резолюция + унификация) 3. Альтернативная трактовка импликации и соответствующая ей новая форма E-диалогов, вносящая дополнительную ассиметрию между допустимыми ходами игрока и оппонента.

Нашел качественную диссертацию с обзором состояния дел в model checking на 2010й год: Weißenbacher, [2010] "Program Analysis with Interpolants" Вкратце идею проверки моделей можно описать так: мы хотим автоматически верифицировать программы, для этого мы аппроксимируем их моделями, то есть автоматами или системами переходов с конечным набором состояний, задаём спецификацию (обычно в какой-то разновидности пропозициональной темпоральной логики) и с помощью поисковых алгоритмов и эвристик исчерпывающе перебираем состояния модели, проверяя что для них всех спецификация верна. Концептуально этот подход описывается теорией моделей (одним из двух основных разделов логики, второй - это теория доказательств, на которой основана теория типов и proof assistants). Интересно, что в моделчекинге примерно раз в декаду сменяется доминирующая парадигма, в целом его таймлайн выглядит примерно так: * 1980е - зарождение самой идеи MC из работ Эдмунда Кларка по вычислению неподвижных точек для систем доказательств в предикат-трансформерах, использование BDD для компактификации состояний * 1990е - дальнейшее ужатие состояний через partial order reduction, появление предикат-абстракции и CEGAR - методов автоматического конструирования моделей из набора assertions о программе * 2000е - SAT/SMT-революция и уход от BDD, быстрая аппроксимация через интерполяцию Крейга * 2010е - Аарон Брэдли изобретает семейство алгоритмов PDR (property directed reachability), где процесс построения инварианта чередуется и взаимодействует с построением контрпримера, взаимно усекая соответствующие пространства поиска * 2020е - ажиотаж вокруг техник из машинного обучения Первые три декады и основные их идеи расписаны в первых двух с половиной главах диссертации (вторая половина третьей и четвертая главы более технические). #automatedreasoning

Ссылки с последнего слайда: * B. Stroustrup: 21st century C++ Blog@CACM January 2025 * C++ Core Guidelines * Profiles ** B. Stroustrup: Safety Profiles: Type-and-resource Safe programming in ISO Standard C++ ** B. Stroustrup: Profiles syntax ** B. Stroustrup: Profile invalidation eliminating dangling pointers ** Herb Sutter: Lifetime safety: Preventing common dangling * Khalil Estell: C++ Exceptions for Smaller Firmware. CppCon 2024 * Daniela Engert: Contemporary C++ in Action. CppCon 2022 a client server application for displaying video frames with timing constraints * B. Stroustrup: A Tour of C++ (3rd Edition). Addison-Wesley. 2022. * B. Stroustrup: Programming: Principles and Practice using C++. * B. Stroustrup's HOPL papers ** A History of C++: 1979-1991. March 1993 ** Evolving a language in and for the real world: C++ 1991-2006. June 2007 ** Thriving in a Crowded and Changing World: C++ 2006-2020. June 2020