Гамарджоба.

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

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

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

  В этом курсе мы рассмотрим основные, иногда неочевидные результаты типа 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).