Где: Уральский Федеральный Университет, Екатеринбург, Россия
Когда: 29-30 ноября 2016
Постер (скачать)
Описание:
Гомотопическая теория типов (ГТТ) и унивалентные основания математики (УО) – это относительно новая и быстро развивающаяся область исследований на пересечении математики, логики, философии и компьютерных наук. Конференция в УрФУ 29-30 ноября – это первая в России конференция, специально посвященная этой теме. Конференция начнется с вводных лекций (тьюториалов), которые позволят всем участникам получить базовые знания в данной области. В оставшееся время будут представлены научные доклады, касающиеся логических, эпистемологических, исторических и вычислительных аспектов ГТТ-УО и теории типов в более общем смысле. Мы приглашаем всех интересующихся для участия в конференции в качестве слушателей и дискутантов.
Организаторы: Алексей Кислов (УрФУ), Лев Ламберов (УрФУ), Андрей Родин (ИФРАН и СПбГУ)
Программа:
День 1: Вторник 29 ноября
10:00 – 10:10 : вступительное слово организаторов
10:10 – 13:30 : утренняя сессия : вводные лекции (тьюториалы). (Председатель Алексей Кислов)
10:10 – 11:10 : Лев Ламберов (УрФУ), Лямбда-исчисление и теория типов (презентация)
перерыв 10 мин.
11:20 – 12:20 : Андрей Родин (ИФРАН и СПБГУ), Гомотопическая теория типов (ГТТ) и аксиома унивалентности
перерыв 10 мин.
12:30 – 13:30 : Даня Рогозин (МГУ), Пруверы Кок и Агда и унивалентные основания математики (презентация)
13:30 – 15:00 – обед
Материалы к тьюториалам:
Pelayo & Warren: HOMOTOPY TYPE THEORY AND VOEVODSKY’S UNIVALENT FOUNDATIONS
NEW! Видео тьюториалов (на ютубе). Дисклэймер: К сожалению, оператор видеокамеры не совсем правильно понял поставленную задачу и сделал получасовой клип, состоящий из фрагментов наших лекций 🙂 Клип хорошо передает атмосферу, а знатокам позволит понять и основное содержание лекций.
15:00 – 17:30 : вечерняя сессия : научные доклады (Председатель Андрей Родин)
15:00 – 15:45 : Алексей Кислов (УрФУ), Конструируя рассуждения (резюме)
15:45 – 16:30 : Виталий Целищев (ИФиП СО РАН), Разветвленная теория типов и подстановочная теория Рассела: почему выбор в Principia Mathematica пал на первую
16:30 – 16:45 перерыв ОТМЕНА
16:45 – 17:30 Александр Хлебалин (ИФиП СО РАН), Логика теории типов
День 2: Среда 30 ноября
10:00 – 13:30 : утренняя сессия : научные доклады (Председатель Алексей Кислов)
10:00 – 10:45 : Татьяна Козьякова (УрФУ), Реализации идеи универсальной характеристики Лейбница в альтернативных подходах к основаниям математики (резюме)
10:45 – 11:30 : Лев Ламберов (УрФУ), Теория типов и теория множеств: к вопросу оснований математики (презентация)
11:30 – 12:00 – кофе
12:00 – 12:45 : Андрей Родин, (ИФ РАН и СПбГУ), Модели гомотопической теории типов и семантический подход к научным теориям (презентация)
12:45 – 13:30 : Даня Рогозин (МГУ), О двух системах типизации (полиморфная и зависимая) лямбда-исчисления и их реализации в функциональном программировании (презентация)
13:30 – 15:00 – обед
15:00 – 17:00 : вечерняя сессия : Круглый Стол (заключительная общая дискуссия)