to post messages and comments.

@OCTAGRAM:

Вынос лемм в отдельные пакеты

@ymn:
Coq

Только что узнал про github.com

Мир никогда не будет таким как раньше, да.

@ymn:
Coq

robbertkrebbers.nl — Robbert Krebbers. The C standard formalized in Coq. PhD thesis. Radboud University Nijmegen

@ymn:
Coq

Нашел интересное чтиво: "Building Verified Program Analyzers in Coq" irisa.fr

@ymn:
Coq

Всем coq-blog.clarus.me например.

@Zert:

twitter.com

@Zert:

Короче, чувак, занимающийся зависимыми типами и доказательствами теорем, говорит, что надо писать тесты и делать код ревью. Шах и мат.

@Zert:

Чувак как-то не особо рассказчик, похоже. Ничего не понятно.

@Zert:

Чувак рассказывает про зависимые типы и петуха: plus.google.com

@Zert:

Чувак по фамилии Идрисов будет рассказывать про Coq: techtalks.nsu.ru
Где логика?

@Zert:

*хз
Нужен (не срочно, но час X всё ближе и ближе) экстрактор в ерланг из каких-нибудь зависимых типов. Ничего не нашёл. Есть чо?

@dukkha:

A program without a specification cannot be incorrect, it can only be surprising.

@ymn:

arxiv.org Все в танк!

@ymn:

Looking for collaborators to develop a formally verified implementation for R7RS (small) using Coq. lists.scheme-reports.org

@ymn:

blog.ezyang.com

@ymn:
Coq

Сабж перевели на гит, например. Пруф — coq.inria.fr

@ymn:

Привет, чятик! Общеизвестно, что эрланг, с точки зрения теории типов и прочего матана, довольно поганенький язык, на котором надоедает писать после полугода активного использования. Поэтому последнюю неделю я активно ковырял широко известный в узких кругах экстрактор CoreErlang github.com для Coq. Так вот, оно риальне работает. С некоторыми ограничениями, конечно, но работает.

@ymn:
Coq

Xenius: Так объясните, что хорошего в Coq? Ну то есть если там нельзя даже hello world вывести... что в нём можно делать?

Xenius: окамл диалект лиспа?

Xenius: Это Scala — диалект лиспа, который компилит в JVM

zert: давайте вконтакте паблик COQ создадим?

Это и многое другое ждет вас в гламурном чятике [email protected]

@Zert:
Coq

[email protected]
первым пяти посетителям звание овнера в подарок.
заходи, если не лох.

@ymn:

Coq для верификации железа: dropbox.com

@ymn:

<gds> проверка императивного алгоритма буферизованного чтения: gds.livejournal.com (Coq, OCaml)
<f[x]> "тогда я взял coq"
<gds> и твёрдо сжал его правой рукой.
<gds> после нескольких несложных действий я понял, что всё реально, всё в моих руках, и конец будет достигнут.

chatlogs.jabber.ru

@Zert:

Петух -> Хвашкиль -> Елангм: sole.dimi.uniud.it
Этого мне и не хватало!

@ymn:

Рабочий экстрактор в недоэрланг для Coq — github.com И еще вот ссылка maxim.livejournal.com

@ymn:

Годный список литературы, который разбирал один задрот в рамках работы над диссертацией про эффекты в кок — guillaume.claret.me

@ymn:
Coq

написал рабочую штуку на coq. ошпарил ноги кипятком)

@ymn:
Coq

вылез из криокамеры и нашел интересное чтиво — Verifying a parser for a C compiler — gallium.inria.fr

@yurlin:

а вот и пост в жж у thedeemon про OPLSS'12:
thedeemon.livejournal.com
посмотрим, что там в комментах ещё напишут.
Но mp4-видео там, правда, тяжёлые.

я когда-то ссылку кидал на curriculum оттуда в #2148509
Да и в этом году будет много всего интересного:
cs.uoregon.edu

@qrilka:

sphotos-b.xx.fbcdn.net

@ygrek:

The Microsoft Research Verified Software Milestone Award is made to Xavier Leroy for the CompCert Project.
dream.inf.ed.ac.uk

@ygrek:

Убил полдня чтобы выяснить что рабочего нативного metaocaml на amd64 сейчас нет, зато спровоцировал gds на очередной сеанс coqционизма : gds.livejournal.com

@folone:

Coq2Scala -> proofcafe.org
Hellyeah!

@jtootf:

seas.harvard.edu — верификатор нативного кода на Coq, или зачем в продакшене зависимые типы

@qrilka:

чего только на связке по тэгам этого поста не понаделают — logitext.ezyang.scripts.mit.edu