В эти выходные в Computer Science клубе (Фонтанка 27 (ПОМИ РАН), второй этаж, мраморный зал) начнется сразу два курса:
"Введение в язык формальной верификации Coq"
Лектор: Антон Трунов, Zilliqa Research
Время начала: суббота, 21 сентября, 15:30
"Структуры данных, основанные на указателях"
Лектор: Елена Арсеньева, СПБГУ
Время начала: суббота, 21 сентября, 17:15
Аннотация курса "Введение в язык формальной верификации Coq":
В первой части мы обсудим формальные доказательства и Coq в общем, разберемся для чего он нужен, где применяется, его место среди других инструментов формальной верификации, затронем экосистему Coq, а также рассмотрим методы связи верифицированных программ и исполняемого кода, такие как экстракция и эмбединг.
Во второй части посмотрим на многочисленных примерах на особенности Coq как языка программирования. В процессе обсудим слабую/сильную нормализацию, зависимые типы, тактики, тотальность, строгую позитивность, иерархию вселенных типов, непредикативность, различия между Type и Prop, экстракцию.
https://compsciclub.ru/courses/intro-to-coq/2019-autumn/
Аннотация курса "Структуры данных, основанные на указателях" :
Мы поговорим о структурах данных, основанных на указателях.
Допустим у нас есть массив чисел, и мы хотим эффективно выполнять поиск в нем, добавлять и удалять элементы. В этом нам помогут деревья поиска, которых существует много разновидностей. Мы обсудим некоторые из них. Как сравнить эффективность разных деревьев? Что такое динамическая оптимальность и какие деревья самые конкурентные по отношению к последовательностям запросов?
А если у нас вместо исходного массива чисел дано дерево, лес, граф? Мы обсудим структуры данных для этих случаев.
Во второй части курса мы посмотрим на общие вопросы о структурах данных основанных на указателях: Если у нас есть статическая такая структура, как сделать ее динамической, и сколько придется за это заплатить? Если у нас есть динамическая структура, можем ли мы так ее модифицировать, чтобы научиться смотреть на ее версии в прошлые моменты времени? Изменять эти версии?
В данном мини-курсе прозвучат ответы на эти и другие вопросы, а также новые вопросы, на которые мы пока не знаем ответа.
https://compsciclub.ru/courses/data-structures-pointers/2019-autumn/
"Введение в язык формальной верификации Coq"
Лектор: Антон Трунов, Zilliqa Research
Время начала: суббота, 21 сентября, 15:30
"Структуры данных, основанные на указателях"
Лектор: Елена Арсеньева, СПБГУ
Время начала: суббота, 21 сентября, 17:15
Аннотация курса "Введение в язык формальной верификации Coq":
В первой части мы обсудим формальные доказательства и Coq в общем, разберемся для чего он нужен, где применяется, его место среди других инструментов формальной верификации, затронем экосистему Coq, а также рассмотрим методы связи верифицированных программ и исполняемого кода, такие как экстракция и эмбединг.
Во второй части посмотрим на многочисленных примерах на особенности Coq как языка программирования. В процессе обсудим слабую/сильную нормализацию, зависимые типы, тактики, тотальность, строгую позитивность, иерархию вселенных типов, непредикативность, различия между Type и Prop, экстракцию.
https://compsciclub.ru/courses/intro-to-coq/2019-autumn/
Аннотация курса "Структуры данных, основанные на указателях" :
Мы поговорим о структурах данных, основанных на указателях.
Допустим у нас есть массив чисел, и мы хотим эффективно выполнять поиск в нем, добавлять и удалять элементы. В этом нам помогут деревья поиска, которых существует много разновидностей. Мы обсудим некоторые из них. Как сравнить эффективность разных деревьев? Что такое динамическая оптимальность и какие деревья самые конкурентные по отношению к последовательностям запросов?
А если у нас вместо исходного массива чисел дано дерево, лес, граф? Мы обсудим структуры данных для этих случаев.
Во второй части курса мы посмотрим на общие вопросы о структурах данных основанных на указателях: Если у нас есть статическая такая структура, как сделать ее динамической, и сколько придется за это заплатить? Если у нас есть динамическая структура, можем ли мы так ее модифицировать, чтобы научиться смотреть на ее версии в прошлые моменты времени? Изменять эти версии?
В данном мини-курсе прозвучат ответы на эти и другие вопросы, а также новые вопросы, на которые мы пока не знаем ответа.
https://compsciclub.ru/courses/data-structures-pointers/2019-autumn/
В этот четверг в Computer Science клубе экперт в распределенных вычислениях и профессор Техниона Шэй Куттен прочитает лекцию "Impacts of Local Checkability".
Абстракт лекции:
In this talk, I outline the notion of local checkability and point at various ways this has proven useful. Local checking (or local verification, or local decision, or local detection, or...) and locally checkable predicates (or languages, or labeling, or ...) were suggested (by Afek, K., and Yuvan, 1990) in the context of self-stabilization. The motivation was the "easy" detection that program malfunctions so that it can be restarted. It was contrasted with the "costly" (i.e. global) checking suggested by Katz and Perry.
It was pointed out that this notion also resembles "easy" checking (or decision, or ...), i.e. polynomial vs. "costly" computing. Indeed, the use of this notion has spread beyond self-stabilization to various fields such as (distributed) complexity theory, distributed testing and peer to peer computing.
https://compsciclub.ru/…/csseminar/2019-autumn/classes/4808/
Лекция пройдет на английском.
Подробнее о лекторе:
https://en.wikipedia.org/wiki/Shay_Kutten
https://compsciclub.ru/users/5717/
Время начала: 26 сентября, 18:30
Место: Фонтанка 27, мраморный зал
Абстракт лекции:
In this talk, I outline the notion of local checkability and point at various ways this has proven useful. Local checking (or local verification, or local decision, or local detection, or...) and locally checkable predicates (or languages, or labeling, or ...) were suggested (by Afek, K., and Yuvan, 1990) in the context of self-stabilization. The motivation was the "easy" detection that program malfunctions so that it can be restarted. It was contrasted with the "costly" (i.e. global) checking suggested by Katz and Perry.
It was pointed out that this notion also resembles "easy" checking (or decision, or ...), i.e. polynomial vs. "costly" computing. Indeed, the use of this notion has spread beyond self-stabilization to various fields such as (distributed) complexity theory, distributed testing and peer to peer computing.
https://compsciclub.ru/…/csseminar/2019-autumn/classes/4808/
Лекция пройдет на английском.
Подробнее о лекторе:
https://en.wikipedia.org/wiki/Shay_Kutten
https://compsciclub.ru/users/5717/
Время начала: 26 сентября, 18:30
Место: Фонтанка 27, мраморный зал
В ближайшие выходные Константин Пашкович (профессор Университета Оттавы) прочтёт курс "Расширенные формулировки" (Extended Formulations)
https://compsciclub.ru/courses/extendedformulation/2019-autumn/
https://compsciclub.ru/courses/extendedformulation/2019-autumn/
14 октября (понедельник) начнётся семинар по тонким оценкам на время работы алгоритмов: https://compsciclub.ru/courses/fine-grained-complexity-seminar/2019-autumn/
Forwarded from Computer Science Center
18 октября в Санкт-Петербурге пройдёт открытая лекция Семёна Григорьева «Теория формальных языков на практике». Приглашаем в БЦ «Таймс» — ул. Кантемировская д. 2, начало в 19:00.
Пожалуйста, зарегистрируйтесь: https://comscicenter.timepad.ru/event/1085032/
Семён — кандидат физико-математических наук, руководитель группы в лаборатории языковых инструментов JetBrains Research и доцент кафедры информатики СПбГУ. Занимается теорией формальных языков и её применениями уже десять лет.
Приходите на лекцию, если вы:
— знаете теорию формальных языков и хотите применять эти знания;
— не знаете теорию формальных языков, но хотите найти мотивацию узнать;
— любите алгоритмы синтаксического анализа и думаете, что же такое написать, чтобы не получился ещё один Yacc.
Запросы к графовым базам данных, алгоритмы статического анализа и верификации кода — примеры практического применения теории формальных языков и алгоритмов синтаксического анализа. В этом контексте возникают новые инженерные и теоретические задачи, а многие старые требуют новых решений. Об этом и пойдёт речь на лекции.
Пожалуйста, зарегистрируйтесь: https://comscicenter.timepad.ru/event/1085032/
Семён — кандидат физико-математических наук, руководитель группы в лаборатории языковых инструментов JetBrains Research и доцент кафедры информатики СПбГУ. Занимается теорией формальных языков и её применениями уже десять лет.
Приходите на лекцию, если вы:
— знаете теорию формальных языков и хотите применять эти знания;
— не знаете теорию формальных языков, но хотите найти мотивацию узнать;
— любите алгоритмы синтаксического анализа и думаете, что же такое написать, чтобы не получился ещё один Yacc.
Запросы к графовым базам данных, алгоритмы статического анализа и верификации кода — примеры практического применения теории формальных языков и алгоритмов синтаксического анализа. В этом контексте возникают новые инженерные и теоретические задачи, а многие старые требуют новых решений. Об этом и пойдёт речь на лекции.
В ближайшие выходные Даниил Рогозин (МГУ, Serokell) прочтёт курс "Введение в модальную логику".
Подробное описание и расписание: https://compsciclub.ru/courses/modal-logic/2019-autumn/
Подробное описание и расписание: https://compsciclub.ru/courses/modal-logic/2019-autumn/
Forwarded from Computer Science Center
В эту пятницу пройдёт первый день открытых дверей на факультете математики и компьютерных наук СПбГУ. Расскажите братьям, сёстрам, знакомым или приходите сами, чтобы узнать, как и на какие программы можно поступить в этом году.
Приходите на очный день открытых дверей в Петербурге. Руководители направлений и организаторы факультета расскажут про учебные программы, курсы, преподавателей, практики и поступление. Готовьте вопросы :)
Место: актовый зал Института наук о земле, 10-я линия ВО, 33-35
Время: 25 октября, пятница, 19:00
Вход свободный. Пожалуйста, зарегистрируйтесь: https://docs.google.com/forms/d/e/1FAIpQLSdH-RXGiJU3BJPskVHIYdgQYK-COSetBCU4Vs8ZSk5l4RW5yw/viewform
Приходите на очный день открытых дверей в Петербурге. Руководители направлений и организаторы факультета расскажут про учебные программы, курсы, преподавателей, практики и поступление. Готовьте вопросы :)
Место: актовый зал Института наук о земле, 10-я линия ВО, 33-35
Время: 25 октября, пятница, 19:00
Вход свободный. Пожалуйста, зарегистрируйтесь: https://docs.google.com/forms/d/e/1FAIpQLSdH-RXGiJU3BJPskVHIYdgQYK-COSetBCU4Vs8ZSk5l4RW5yw/viewform
В эти выходные в Computer Science Клубе пройдет курс "Алгоритмическая теория игр".
Лектор: Михаил Николаевич Вялый
https://compsciclub.ru/teachers/1050/
Подробное описание и расписание:
https://compsciclub.ru/courses/algo-game-theory/2019-autumn/
Лектор: Михаил Николаевич Вялый
https://compsciclub.ru/teachers/1050/
Подробное описание и расписание:
https://compsciclub.ru/courses/algo-game-theory/2019-autumn/
Forwarded from Computer Science Center
Напоминаем, что 14 ноября начнётся обучение на полугодовых онлайн-программах по направлениям
— Алгоритмы и эффективные вычисления,
— Математика для разработчиков,
— Разработка на C++, Java и Haskell.
Что ждёт студентов:
— Курсы от опытных разработчиков и учёных.
— Задачи, чтобы закрепить изученный материал.
— Code review. Преподаватели оценивают код на корректность, эффективность и поддерживаемость.
— Теоретические задачи на доказательство с проверкой от преподавателей.
— Персональная поддержка. Ассистенты и преподаватели помогут разобраться с материалом, а кураторы будут следить за успеваемостью.
Набор на программу идёт по результатам вступительных испытаний: сначала мы предложим пройти первый модуль одного из курсов, чтобы вы познакомились с материалом, форматом и оценили нагрузку. Вторым этапом будет экзамен по профильному предмету. Дедлайн — 10 ноября.
Стоимость программы — 20 000 рублей. Принять участие во вступительных испытаниях, прочитать отзывы выпускников и узнать больше можно на сайте: http://code.stepik.org/
— Алгоритмы и эффективные вычисления,
— Математика для разработчиков,
— Разработка на C++, Java и Haskell.
Что ждёт студентов:
— Курсы от опытных разработчиков и учёных.
— Задачи, чтобы закрепить изученный материал.
— Code review. Преподаватели оценивают код на корректность, эффективность и поддерживаемость.
— Теоретические задачи на доказательство с проверкой от преподавателей.
— Персональная поддержка. Ассистенты и преподаватели помогут разобраться с материалом, а кураторы будут следить за успеваемостью.
Набор на программу идёт по результатам вступительных испытаний: сначала мы предложим пройти первый модуль одного из курсов, чтобы вы познакомились с материалом, форматом и оценили нагрузку. Вторым этапом будет экзамен по профильному предмету. Дедлайн — 10 ноября.
Стоимость программы — 20 000 рублей. Принять участие во вступительных испытаниях, прочитать отзывы выпускников и узнать больше можно на сайте: http://code.stepik.org/
Forwarded from Computer Science Center
Приглашаем на открытую лекцию Артёма и Антона Филатовых «Введение в алгоритмы одновременной локализации и построения карты (SLAM)». Она пройдёт 25 ноября в 19:00 в БЦ «Таймс» в Санкт-Петербурге. Адрес: Кантемировская 2А, 2 этаж, ауд. 204.
Пожалуйста, зарегистрируйтесь: https://comscicenter.timepad.ru/event/1120066/#register
Артём и Антон — программисты-исследователи научно-исследовательского и образовательного центра «ДжетБрейнс», ассистенты кафедры МОЭВМ в СПБГЭТУ (ЛЭТИ).
Среди задач, которые уже решают роботы, спикеры выделяют задачу автономного перемещения по неизвестной местности. Когда движущийся робот оказывается в неизвестном окружении, ему нужно построить карту и определить на ней своё положение, опираясь на данные сенсоров, установленных на роботе. Такая задача называется SLAM (Simultaneous Localization and Mapping).
На лекции Артём и Антон рассмотрят большую часть современных алгоритмов, которые решают задачу SLAM, расскажут про решённые и нерешённые вопросы в рамках этой задачи, а также покажут решение такой задачи на практике. Правда, в симуляторе :)
Пожалуйста, зарегистрируйтесь: https://comscicenter.timepad.ru/event/1120066/#register
Артём и Антон — программисты-исследователи научно-исследовательского и образовательного центра «ДжетБрейнс», ассистенты кафедры МОЭВМ в СПБГЭТУ (ЛЭТИ).
Среди задач, которые уже решают роботы, спикеры выделяют задачу автономного перемещения по неизвестной местности. Когда движущийся робот оказывается в неизвестном окружении, ему нужно построить карту и определить на ней своё положение, опираясь на данные сенсоров, установленных на роботе. Такая задача называется SLAM (Simultaneous Localization and Mapping).
На лекции Артём и Антон рассмотрят большую часть современных алгоритмов, которые решают задачу SLAM, расскажут про решённые и нерешённые вопросы в рамках этой задачи, а также покажут решение такой задачи на практике. Правда, в симуляторе :)
Курс посвящен теории, лежащей в основе современных промышленных распределенных систем: файловых систем, очередей сообщений, key/value хранилищ, баз данных. Эти системы хранят десятки и сотни петабайт данных, обслуживают многие тысячи запросов в секунду и масштабируются до сотен и тысяч машин, переживая при этом отказы дисков и питания, дрейф часов, задержки и нарушения связности сети, а потому устроены невероятно сложно.
Но если посмотреть сквозь все инженерные детали и сотни тысяч строк кода, то окажется, что сложность, связанную с распределенностью, можно заключить в относительно простые модели и задачи: как узлам договориться о порядке доставки сообщений в асинхронной сети, как выбрать лидера среди равноправных машин, как добавить в систему еще один сервер или обнаружить сбойную машину. Именно от решения этих задач в конечном итоге будут зависеть важнейшие характеристики всей системы: границы ее отказоустойчивости, доступность при нестабильном поведении сети, модель согласованности данных.
В курсе мы сформулируем эти задачи, исследуем ограничения, которые накладывает на них модель сети и сбоев, и подробно разберем алгоритмы их решения, которые применяются в современных промышленных распределенных системах.
Лекции будут выстроены в одну историю: мы начнем с выбора модели распределенной системы и очень простой задачи построения отказоустойчивой ячейки памяти, на примере которой изучим ключевые техники дизайна распределенных алгоритмов, затем перейдем к общему механизму репликации через Atomic Broadcast и изучим его связь с задачей консенсуса и ключевые результаты о невозможности, подробно разберем известный алгоритм Paxos и выведем из него Multi-Paxos или RAFT, а завершим курс византийской моделью и Bitcoin-ом, на который посмотрим через призму изученных ранее классических результатов и алгоритмов.
https://compsciclub.ru/courses/distributed-computing/2019-autumn/
Но если посмотреть сквозь все инженерные детали и сотни тысяч строк кода, то окажется, что сложность, связанную с распределенностью, можно заключить в относительно простые модели и задачи: как узлам договориться о порядке доставки сообщений в асинхронной сети, как выбрать лидера среди равноправных машин, как добавить в систему еще один сервер или обнаружить сбойную машину. Именно от решения этих задач в конечном итоге будут зависеть важнейшие характеристики всей системы: границы ее отказоустойчивости, доступность при нестабильном поведении сети, модель согласованности данных.
В курсе мы сформулируем эти задачи, исследуем ограничения, которые накладывает на них модель сети и сбоев, и подробно разберем алгоритмы их решения, которые применяются в современных промышленных распределенных системах.
Лекции будут выстроены в одну историю: мы начнем с выбора модели распределенной системы и очень простой задачи построения отказоустойчивой ячейки памяти, на примере которой изучим ключевые техники дизайна распределенных алгоритмов, затем перейдем к общему механизму репликации через Atomic Broadcast и изучим его связь с задачей консенсуса и ключевые результаты о невозможности, подробно разберем известный алгоритм Paxos и выведем из него Multi-Paxos или RAFT, а завершим курс византийской моделью и Bitcoin-ом, на который посмотрим через призму изученных ранее классических результатов и алгоритмов.
https://compsciclub.ru/courses/distributed-computing/2019-autumn/
В эти выходные в клубе начнется курс "Теоретико-числовые алгоритмы и криптография".
Подробное описание:
https://compsciclub.ru/courses/numbertheory-algo/2019-autumn/
Подробное описание:
https://compsciclub.ru/courses/numbertheory-algo/2019-autumn/