AV
буду очень признателен если будет запись, очень жалко но таки не доеду до Питера сегодня
Size: a a a
2018 May 31
2018 June 02
AE
Вы просили — мы сделали: в этом месяце никакого Хаскел!
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.
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.
Вдруг кто-нибудь да прочитает
Список рекомендованной литературы из доклада @niquola "Make frontend backend again"
Fred Brooks "No Silver Bullit" http://worrydream.com/refs/Brooks-NoSilverBullet.pdf
Roy Fielding "Architectural Styles and the Design of Network-based Software Architectures" https://www.ics.uci.edu/~fielding/pubs/dissertation/fielding_dissertation.pdf
Ben Moseley, Peter Marks "Out of the Tar Pit" http://curtclifton.net/papers/MoseleyMarks06a.pdf
Список рекомендованной литературы из доклада @niquola "Make frontend backend again"
Fred Brooks "No Silver Bullit" http://worrydream.com/refs/Brooks-NoSilverBullet.pdf
Roy Fielding "Architectural Styles and the Design of Network-based Software Architectures" https://www.ics.uci.edu/~fielding/pubs/dissertation/fielding_dissertation.pdf
Ben Moseley, Peter Marks "Out of the Tar Pit" http://curtclifton.net/papers/MoseleyMarks06a.pdf
AZ
Спасибо.
2018 June 07
b
[анонс][x-post ruHaskell][освящено Игнатом]
Этим летом в GoTo снова будет Чёрная Лямбда, а то и не одна. Если вам давно хотелось Coq и старшеклассников, или вносить Haskell (и даже Liquid) по четыре пары в день в студенческие минимассы, или вы готовы рассказывать про верифицированную криптографию и сети на FPGA и на коне - поговорим про это! Сайтики на Clojure тоже in scope. Школы пройдут 17-30, 15-28 и 12-25 летних месяцев соответственно, в Подмосковье. Можно доить коз.
[Чёрная]: https://habr.com/company/goto/blog/333828/
[Лямбда]: https://habr.com/company/goto/blog/351496/
[Анонс трека]: https://gateway.ipfs.io/ipfs/QmUpXj4dfCEiBRkXLEejL2Fz78Zqy9Fi8yRqN17bVGu8YC/
Этим летом в GoTo снова будет Чёрная Лямбда, а то и не одна. Если вам давно хотелось Coq и старшеклассников, или вносить Haskell (и даже Liquid) по четыре пары в день в студенческие минимассы, или вы готовы рассказывать про верифицированную криптографию и сети на FPGA и на коне - поговорим про это! Сайтики на Clojure тоже in scope. Школы пройдут 17-30, 15-28 и 12-25 летних месяцев соответственно, в Подмосковье. Можно доить коз.
[Чёрная]: https://habr.com/company/goto/blog/333828/
[Лямбда]: https://habr.com/company/goto/blog/351496/
[Анонс трека]: https://gateway.ipfs.io/ipfs/QmUpXj4dfCEiBRkXLEejL2Fz78Zqy9Fi8yRqN17bVGu8YC/
DR
> Если вам давно хотелось Coq и старшеклассников
DR
чудо-графоманы
b
> fprog_spb
> Подмосковье
наверное достаточно было просто в общеязыковых чатах осветить
> Подмосковье
наверное достаточно было просто в общеязыковых чатах осветить
Речь именно про ФП и верификацию.
b
чудо-графоманы
NOTABUG
DR
в днк баг
PK
Это он мне. Я не учусь в политехе.
Вл
Это он мне. Я не учусь в политехе.
ясно, спасибо