Coq Как же смешно гуглить "coq injection". (На самом деле гугол уже знает мои вкусы, а вот дакдак предлагает смешное).

math Coq Читаю Coq'Art. Доказал только что очередной (достаточно очевидный) факт, и внезапно захотелось поделиться и успехом (это было не очень просто), и мыслями на тему. А за одно решил обновить бложек на blogger. А чтобы не править по 10 раз для разных мест то тут просто оставлю ссылку. Поэтому под кат — это сюда

Coq Доказал коммутативность умножения на натуральных числах. Это было не тривиально, мать его.

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

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

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

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

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

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

Coq Perl Haskell twitter.com

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

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

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

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

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

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

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

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

Coq Haskell blog.ezyang.com

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

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

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

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

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

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

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

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

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

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

chatlogs.jabber.ru

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

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

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

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

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

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

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

Java Coq Agda Haskell sphotos-b.xx.fbcdn.net

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

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

Scala Coq link Coq2Scala -> proofcafe.org
Hellyeah!

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

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