Чтобы добавлять сообщения и комментарии, .

@ymn:
ymn

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

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

@ymn:
ymn

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

@ymn:
ymn

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

@ymn:
ymn

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

@Zert:
Zert

twitter.com

@Zert:
Zert

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

@Zert:
Zert

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

@Zert:
Zert

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

@Zert:
Zert

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

@Zert:
Zert

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

@dukkha:
dukkha

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

@ymn:
ymn

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

@ymn:
ymn

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

@ymn:
ymn

blog.ezyang.com

@ymn:
ymn

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

@ymn:
ymn

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

@ymn:
ymn

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

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

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

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

Это и многое другое ждет вас в гламурном чятике coq@c.j.r

@Zert:
Zert

coq@conference.jabber.ru
первым пяти посетителям звание овнера в подарок.
заходи, если не лох.

@ymn:
ymn

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

@ymn:
ymn

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

chatlogs.jabber.ru

@Zert:
Zert

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

@ymn:
ymn

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

@ymn:
ymn

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

@ymn:
ymn

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

@ymn:
ymn

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

@yurlin:
yurlin

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

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

@qrilka:
qrilka

sphotos-b.xx.fbcdn.net

@ygrek:
ygrek

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

@ygrek:
ygrek

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

@folone:
folone

Coq2Scala -> proofcafe.org
Hellyeah!

@jtootf:
jtootf

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

@qrilka:
qrilka

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