• 13 октября 2016
  • Санкт-Петербург, Большой Сампсониевский просп. 60А, офис DataArt

FProg (Октябрь 2016)

Регистрация на событие закрыта

Извините, регистрация закрыта. Возможно, на событие уже зарегистрировалось слишком много человек, либо истек срок регистрации. Подробности Вы можете узнать у организаторов события.

Другие события организатора

200 дней назад
13 октября 2016 c 19:00 до 23:00
Санкт-Петербург
Большой Сампсониевский просп. 60А, офис DataArt

Октябрьская встреча любителей и профессионалов функционального программирования в Санкт-Петербурге, посвящённая зависимым типам и автоматическому доказательству теорем.

Idris: неужели дождались? — Игнат Толчанов

Несмотря на то, что зависимые типы — концепция далеко не новая, большей части разработчиков они неизвестны, большей части остальных же они кажутся драматически далёкими от их реальных проблем. Не в последнюю очередь эта ситуация сложилась благодаря инструментам и языкам программирования, ориентированным в большей степени на исследовательскую работу, нежели на коммерческую разработку. Но несколько лет назад появился Idris: язык с поддержкой зависимых типов, задуманный как язык программирования общего назначения.

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


Доказательство свойств программ — введение в Coq — Андрей Ляшин

1. Тестирование vs Доказательство.

2. Какие программы можно доказать (индуктивные типы, конструктивные построения, интуиционисткая логика, и структурно редуцирующая рекурсия)?

3. Почему это возможно (изоморфизм Карри-Ховарда и все такое)?

4. Что доказать нельзя (Тьюринг полнота и обязательна ли она)?

5. Как сформулировать доказываемую спецификацию?

6. Это упрощает или усложняет жизнь?

7. Что делать, если понравилось?

 

В унисон с поющим драконом: ответы на ЧаВо (Idris) — Антон Трунов

1. От пустого типа к семействам типов: неформальное введение.

2. А нам не всё равно: разбираемся с `=`, `==` и `decEq`.

3. Используй тотальные функции, Люк: примеры.

4. Боремся за тотальность строго и положительно: strict positivity.

5. Доверяй, но проверяй: верифицированные функторы, аппликативные функторы и монады.

6. Как перестать беспокоиться о хвостовой рекурсии и начать жить: пишем `map`.


Афтепати
В Puberty 


Программа встречи может быть уточнена

Регистрация

Рекомендуемые события

Организуете события? Обратите внимание на TimePad!

Профессиональная билетная система, статистика продаж 24/7, выгрузка списков участников, встроенные инструменты продвижения, личный кабинет для самостоятельного управления и еще много чего интересного.

Узнать больше