*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

>В любом случае, если вы хотите узнать о теории типов, купите книгу "Типы и Языки Программирования" от Бенджамина Ф. Пирса. Если вы всё ещё запутались, вы можете развеять все трудности с помощью "Продвинутых Вопросов в Типах и Языках Программирования" от Бенджамина Ф. Пирса. Предположительно, Профессор Пирс сейчас ... more →

#titnfg

1 comment

"
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

Вы тупое, убогое, безграмотное ничтожество.

Повторяю, свинья, проблема P=NP не имеет ни малейшего отношения к нечеткой логике. Это во первых. Во вторых, нечеткая логика имеет самое непосредственное отношение к математике.

Ну да у вас же IQ явно меньше 50, смысла вам что либо объяснять нет. Вы всего лишь убогая ... more →

#tfgsoe

add comment

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

#tfestg

2 comments

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

#tfifzf

add comment

http://plasmon.rghost.ru/42048577/image....

#tfhess

2 comments

Normalized Device Coordinates → Нормализованное пространство приборных координат
Ничотак перевод, да?

#thgitz

add comment

посоны где скачать контру 1.6?

#thsigf

2 comments

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

#thfgnh

1 comment

Кто тут в кемперстрайк играет? Реквестирую советов по поводу того, как не быть дном

#tthfzn

2 comments

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

#toehgt

18 comments

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

#tosifn

3 comments

http://web.mit.edu/newsoffice/2012/inter...

#tzsgfn

add comment

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

#tzzffo

9 comments

http://i.imgur.com/Wx91Z.jpg

#onnioe

1 comment

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

#onzfeg

5 comments

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

#oggssf

1 comment