*cs

"thunk" / "deferred computation" — "личинка вычисления".
Соответственно, при использовании лентяйки программа откладывает в память личинки вычислений.
//
"use" — "использование". "abuse" — "извредствование"?

#tseohz

2 comments

Зарелизил мелкую библиотечку для отладки редукций выражений в пределах coq: https://bitbucket.org/gds/coq-breakpoint...

#tsszng

6 comments

Посоны, помогите с задачкой. Я совсем разучился в графы. Наговнокодить могу, но должно быть красивое решение (скорее всего, ещё и более быстрое, чем наивный говнокод).
Есть направленный ациклический граф: https://docs.google.com/drawings/d/1OPIv...
Задана ... more →

#tsigii

17 comments

Наша редакция рада ответить на просьбу господина @ulidtko, изложенную в http://amd63.psto.net/tsfgse#123 , нижеследующим куском кода: https://gist.github.com/gdsfh/7140f41aca...
Там в каментах я показал, во что экстрактится всё это безобразие. Как обычно, все пруф-термы стёрты, остались только ... more →

#tsiezf

2 comments

Пост про различие "proof of negation" vs "proof by contradiction", в том числе есть интересное про отличие классической от интуиционистской (конструктивной) логики (однако, если последнее вам известно, в том числе на практике, то читать будет не очень интересно, разве что для структуризации знаний): ... more →

#tstsgt

add comment

"построение термов тактиками в coq — безопасно" [ http://gds.livejournal.com/66182.html ]

#tinhoi

add comment

"Можно [...] самим попытаться двинуть науку в бок, потому что вперед не можем, а назад не разрешают :-)" [lj\maxim]

#tiinit

1 comment

"
There are only two hard things in Computer Science: naming things, cache invalidation and off-by-one errors.
"
[lj\wizzard0]

#tihiti

10 comments

"
This reminds me of a funny event at the Haskell workshop 2006. One participant stood up and sincerely proposed that Haskell' standard would find a way to automatically derive a monadic version of a pure expression. Chung-chieh Shan recommended that person to take a look at OCaml...
"
(уже второй раз лезу за этой ... more →

#tioeof

add comment

При создании рекурсивных структур данных часто используется приём, известный как "tying the кот".

#tfestg

2 comments

Coq quick reference: https://wiki.mq.edu.au/display/plrg/Reso...

#tfifzf

add comment

Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО < http://gds.livejournal.com/65879.html >

#thfgnh

1 comment

Постил в камлочятик, но запощу и тут.
Есть вероятность, что Олег будет давать интервью. Можно повлиять на вопросы. Присылайте мне, я передам куданадо.
Вопрос про то, не жмёт ли ему череп, я задать хотел бы, но это некультурно. Вопрос про будущее метаокамла уже скинул. Вопрос про субъективное сравнение языков с ... more →

#toehgt

18 comments

"гулял в компании зависимых типов"

#tosifn

3 comments

#coq:
ianjneu: Javascript and Python have nonsense-ical scope. A colleague says, "they don't have lexical scope. They have kaleidoscope."

#tzzffo

9 comments

К нам сегодня заходил
Лиспомакроскобкофил,
Он межушным поролоном
Типизацию хулил.

#onzfeg

5 comments

Офигенная штука: http://logitext.ezyang.scripts.mit.edu/l... — интерактивная обучалка sequent calculus, и, в том числе, "Невыносимо-Непонятного Контекста Γ".

#oggssf

1 comment

#coq:
(2012-04-24 20:40:40) apfelmus вышел из комнаты (quit: Quit: (λx.xx)(λx.xx)).

#oenezg

add comment

спрашивал в камлочятике, но спрошу и тут.
У кого-нибудь есть желание и возможность совместно поработать над типизированной императивщиной для atmega-подобных мелочей в рамках coq? Нужен в том числе опыт писания под эти или подобные мелкие процессоры. (если не знаете coq, но владеете функциональщиной — заодно ... more →

#oegefo

3 comments

продолжение изложения основ теории категорий в понятном виде: http://thedeemon.livejournal.com/47570.h...

#oeghhg

add comment

"After a few years trying to follow this list, I start to have an idea of what it means when J. Garrigue says that something is difficult  :)" [caml-list]

#oesnhi

add comment

В одном из постов @beardog говорит "тяжело быть идиотом". Не знаю, идиот ли он, но я в этом и сомневаюсь, и считаю это совершенно не важным для текущего поста.
Потому что у меня опять параллели с языками программирования. (кто про что, а я опять про это говно.)
Я считаю, что идиотом быть просто, только последствия ... more →

#oeifhi

6 comments

сейчас наткнулся на подобную штуку, и немного генерализирую.
при написании веб-сервера на coq обнаружим, что рекурсивная функция, читающая http-заголовки, внезапно потребует доказательства завершимости. По идее, оно должно включить в себя конечность числа символов в прочитанных заголовках, либо конечность как числа ... more →

#osgisi

add comment

к моему посту #osofnz — Олег Киселёв пишет в caml-list:
"Somehow typed tagless interpreters (embeddings of a typed language) and length-parameterized lists with the append function are the most popular examples of GADTs. Neither of them seem to be particularly good or compelling examples. One can write typed ... more →

#osehhh

2 comments

ааа, убейте меня, иначе я всё забрызгаю тут1111
@default631">http://flint.cs.yale.edu/cs428/coq/doc/R...
СУТЬ:
У вас есть индуктивный тип данных для представления вашего игрушечного AST, специфичного для вашей предметной области.
У вас есть функция, преобразующая _ваши_ значения из AST в ... more →

#osfnnt

6 comments