ЛЯ
ЛЯ
20
23

Гамарджоба.

Летняя школа сложного программирования и современного искусства.

Одноранговая вечеринка. Инженерия и задор.

40ч курсов
15-23 июля
30ч искусства
близ Тбилиси
A queer person explaining category theory concepts A queer person explaining category theory concepts in space
  1. Выбери фулл-тайм курс

  2. Побудь с творческой программой

  3. Приезжай

Кто все эти люди

Курсы (предварительные)

  • Машинное обучение: золотой граммофон

    Машинное обучение переосмысляет себя на глазах. С текущим числом публикаций в области легко потеряться, если отвлечься на год-другой.

    В этом курсе мы рассмотрим основные, иногда неочевидные результаты типа lottery ticket hypothesis или Deep Q-Learning и реализуем самые сочные статьи, чтобы актуализировать интуицию о происходящем в области и разобраться, как смотреть на текущие исследования.

  • Purescript all the way

    Haskell это круто, но с ним есть известные проблемки. Purescript компактно реализует идеи Haskell и работает в браузере.

    Этот курс проходит от основ функционального программирования и алгебраического моделирования предметной области, исследует VDOM-библиотеку halogen как пример написания реактивного программирования на Purescript, и затем демонстрирует уникальные фичи Purescript (row types, JS FFI), и погружается в его (вполне читаемый!) компилятор.

  • Like a supercollider

    Идея этого курса - изучение языков программирования для создания звука и музыки: низкоуровневых, переводящих функционал DAW в код (SuperCollider) и языков над ними (TidalCycles, Sonic Pi). Вместо того, чтобы пошагово учить языки, мы будем анализировать, смешивать, алгорейвить примеры кода из сети, выбирая нам интересные. Отдельно глянем на синтезаторы визуалов типа Hydra.

    В зависимости от желаний слушателей, можем развернуть программу на 180 и похакатонить: пораскрашивать нотки в music21, сделать поисковый фронтенд к корпусу гармоний When-in-Rome, скрестить Tuttitempi с Maestro, разметить корпус саундтрэков к Sega Genesis и изучить достижения Google Magento. База знаний и канал, откуда можно черпать идеи, находятся в Github и Telegram.

    Также можем провести лекции по теории музыки в разных культурах, но это менее интерактивно.

    Пишите @vitalypavlenko, если хотите участвовать в этом курсе – давайте соберём его вместе.

  • Приключения Логических Интегральных Схем

    В этом курсе мы обсудим основы цифровой схемотехники, посмотрим на современные FPGA включая Versal ACAP, изучим SystemVerilog и сделаем несколько проектов, повышая сложность от мигания светодиодом до VGA и RISC-V.

  • Zero-knowledge proofs

    ZKP - одна из самых захватывающих и ценных теорий, стоящих за Web3. За последние 4-5 лет количество проектов, использующих ZKP, резко возросло – их можно использовать практически везде: от создания доказательств передачи активов до решения проблем масштабируемости. Это делает ZKP новым фронтиром Web3 и децентрализованных систем.

    Цель этого курса - показать математику, стоящую за ZKP, и предоставить некоторые практические знания. Мы погрузимся в современные фреймворки и DSL ZKP и посмотрим на практические применения.

    Требования: базовые знания абстрактной алгебры (группы, генераторы групп), криптографии (цифровые подписи) и алгоритмов. Знание языка программирования Rust (умение читать и писать код с трейтами Fn*) приветствуется.

  • 10 исчислений Isabelle

    В этом курсе мы возьмём один алгоритм и верифицируем его в десяти исчислениях в Isabelle/HOL. Следуя статье, мы построим серию формальных языков, их моделей и доказательств полноты от простого к сложному. В конце построим и докажем корректность алгоритма типа SAT для теории порядков. Для этого соорудим парочку теорий доказательств.

    Для этого курса нужно знать базовое ФП и основы формальной логики.

    В результате курса участник научится строить свои (маленькие) формальные языки, строить интерпретации для них, доказывать soundness and completeness, верифицировать алгоритмы и читать статьи по PLT.

  • SAT / SMT

    SAT-солверы решают NP-сложные задачи.

    По теореме Кука-Левина, NP-сложные задачи сводимы друг к другу. Для некоторых представлений задачи получаются эффективные эвристики; задача SAT – одна из таких.

    На практике это значит, что как будто бы O(n!) задача часто считается.


    Этот курс посвящен CS и теории алгоритмов, которые направлены на решение SAT. Мы рассмотрим задачу SAT и алгоритм CDCL на основе обучения конфликтам, который её эффективно решает. Мы также изучим задачу SMT и алгоритм DPLL – полное и корректное решение SMT на основе алгоритма Дэвиса-Патнема и theory propagation.

    Мы исследуем различные теории, используемые при решении задач SAT/SMT, такие как логика предикатов, булева логика с кванторами, линейная арифметика и логика битовых векторов. Вы получите практический опыт применения этих алгоритмов для решения различных задач, а также узнаете теоретические основы решения задач SAT/SMT.

    Для этого курса нужно базовое понимание математической логики и дискретной математики. В результате курса вы познакомитесь как с теорией, так и с применением солверов на практике.

  • Современные Лиспы

    Грустно ждать пересборки всего проекта, чтобы протестировать небольшое изменение? Не хватает фичей языка? Всегда хотелось нырнуть в Лиспы, но было непонятно, какой взять диалект и откуда начать? Этот курс про ответы на эти вопросы и много лет опыта Лиспов в индустрии.

    ФП уже никого не удивить, но с REPL и TDD, чтобы сразу тестировать и видеть результат, его совмещают не так часто. Вся наша практика будет очень интерактивная, программы интроспектируемые в рантайме, и циклы обратной связи суперкороткими.

    Кроме REPLов, Лиспы также известны своей гомоиконичностью и макросами, и в ходе курса мы будем активно метапрограммировать: добавлять новые фичи в язык и делать data-driven eDSL и интерпретаторы к ним. Будем вкладывать одни диалекты Лиспов в другие, запускать один код на разных рантаймах, делать разметку, вёрстку, запросы к БД, манипуляцию данных – всё в одном языке.

    Также мы кратко пройдём по истории семейства Лиспов и посмотрим, какие фичи идеального Лиспа сейчас есть в разных диалектах.

    В конце концов, мы нырнём в скобочный мир с головой: настроим IDE Лиспом, сделаем веб-приложение Лиспом, опишем ОС Лиспом, и задеплоим тоже Лиспом (Elisp, Clojure(Script), Guile Scheme, Guix).

Обычный день проходит так

9:30Просыпание
9:45Утренняя йога
10:30Завтрак
11:00Семинар
12:15Перерыв
12:30Лекция
13:45Обед
14:30Класс по танцам
15:45Перерыв
16:00Лекция
17:15Полдник
17:30Семинар
18:45Перерыв
19:00Горные велосипеды
20:15Ужин
21:00Ночная прогулка
23:00Подготовка ко сну
0:00Zzz...
A man looking out into the camera while doing coursework on the balcony

Арт-программа

astrology exploration astronomy with telescope
Йога
berry picking bird-watching
Классы по уличным и клубным стилям
campfire cooking contact impro
Классы contemporary импровизации
contemporary dance disc golf
Группа лаборатория
dream analysis drum circle
Контактная импровизация
hiking horse riding
Самопрезентация
house dance kayaking
Импровизация
meditation mountain biking
Лисэнинги
nature photography outdoor painting
Тематические вечеринки
plant identification walk poetry reading
Вечер с играми
rock climbing or bouldering slack-lining
Музыкальные джемы
stargazing survival skills workshop
Конкурс сдохни или умри
swimming teambuilding activities
Cringe day
uterine breathing vision board creation
Вечерний променад по берегу озера
wrestling yoga
Tongue Piano Table Tennis A group of students listening to a lecture on Haskell Virification
scroll me→

Площадка и размещение

Школа пройдёт в Hotels & Preference Hualing Tbilisi, пятизвёздочном отеле у Тбилисского Моря. Море в трёх минутах ходьбы.

Дорога от аэропорта занимает двадцать минут. На автобусе из Еревана можно добраться за пять-шесть часов.

Hualing Hotels & Preference Field Презентация площадки↗
This big

Стоимость участия

Цена включает:

  • Проживание 9 дней и 8 ночей
  • Басейн/сауну/спортзал
  • Шведский стол три раза в день + полдники
  • Круглосуточные перекусы
  • Участие во всех мероприятиях школы

Самостоятельно нужно только добраться. Мы поможем участникам самоорганизовать трансферы из Владикавказа/Батуми/Еревана. Добравшись до Тбилиси, можно просто вызвать такси.

На школе можно жить вместе с другим участником или одному: это то, что значат xxxx/yyyy$. Ещё можно забронировать моднейший номер с джакузи и проспонсировать гранты для других участников, взяв спонсорский билет.

Если вы уже живётё в Тбилиси и вам комфортно ездить на школу, вы можете не платить за проживание в отеле.

Мы просим корпоративных участников платить больше за билет. Это позволяет нам сделать школу более доступной для других участников.

Чтобы посмотреть стоимость своего билета, выберите свой тип участия:

1000$/1300$
March birds
до 12/04/23
1100$/1400$
April bees
до 30/04/23
1400$/1700$
May fedoras
до 15/06/23
2000$/2500$
Late birds
до 09/07
Спонсорский билет: 5555$

Составляющие стоимости

Ticket cost breakdown

Бюджет (без отеля)

Доход loading...
Затраты loading...
Прибыль loading...
Полный расчёт бюджета и прозрачная бухгалтерия↗

Регистрация