FProg October

Встреча / Meetup сайт события https://spb-fp-meetup.timepad.ru/event/377404/

Добавить в календарь:
Поделиться:

Октябрьская встреча сообщества функциональных программистов

 

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

 

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

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

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


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

  1. Тестирование vs Доказательство.
  2. Какие программы можно доказать (индуктивные типы, конструктивные построения, интуиционисткая логика, и структурно редуцирующая рекурсия)?
  3. Почему это возможно (изоморфизм Карри-Ховарда и все такое)?
  4. Что доказать нельзя (Тьюринг полнота и обязательна ли она)?
  5. Как сформулировать доказываемую спецификацию?
  6. Это упрощает или усложняет жизнь?
  7. Что делать, если понравилось?

 

Афтепати В Puberty 

Комментарии (0):

Оставлять комментарии могут только зарегистрированные пользователи

Для получения embed кода необходимо кликнуть правой
кнопкой мыши на видео и выбрать пункт меню
'Сгенерировать HTML код'

 

Забыли пароль? Регистрация