Haskell Haskell NotHaskell

недоCoq недоCoq Coq

Пора пеименоваться в haskell_spb

интереско как можно так нелюбить доклады на haskell и иметь haskell-ную аватарку ;)

У меня есть haskell-кепка, в интернете заказывал

:/ у меня только футболка Tweag I/O

прекрасный пак

Скальных наездников не хватает.

Тут один сплошной Вивек, чего уж там

Всем привет! На ютуб-канале появились видеозаписи с апрельской встречи (ссылка на канал есть в описании чата). Приятного просмотра :)

ееее

❤️

спасибо!

Монтажер постарался на славу. Экранчики переключаются, скрины зумятся

да, молодцы

Вот те раз...
А ссылка где?

bit.ly/fprog_spb-youtube в описании канала ссылки на соцсети

Псб

Вы просили — мы сделали: в этом месяце никакого Хаскел!

31 мая мы встретимся, чтобы послушать про Coq. В программе вечера:

- Неконструктивные расширения Coq, Сергей Божко, работает над доказательством теорем о планировщиках для систем реального времени, студент СПбГУ, в докладе рассмотрит расширения ядра Coq’a. Ядро языка Coq построено на конструктивной логике, которая обеспечивает относительно слабую концепцию равенства. Это контрастирует с большинством других известных систем доказательств теорем (например, Isabelle/HOL), которые основаны на классической логике. Для того, чтобы восстановить данные особенности, можно использовать несколько аксиом.

- Возможности использования формальных верификаций на Coq для простейших моделей смарт-контрактов, Андрей Ляшин, участник стартапа FinProof и популяризатор теории категорий в программировании, рассмотрит реализацию основных функций стандартного токена ERC20 с демонстрацией доказуемости и недоказуемости свойств для корректной и, соответвенно, некорректной реализаций рекурсивных функций переводов, лежащих, в частности, в основе атаки на the DAO.

Регистрация: https://spb-fp-meetup.timepad.ru/event/725191/

Встречаемся в офисе JetBrains по адресу: Университетская наб., 7-9-11, корп. 5 (вход с Кадетской линии), БЦ «Universe».

Время проведения встречи: с 19:00 до 22:00.