*coq

gds 26.03.2013 14:20

Как выяснилось, карго-культ по отношению к PHOAS работает плохо, особенно если нужно делать чуть больше, чем простую лямбду. Чо ж делать-то, а? Может кто-нибудь объяснит потолковее, чем в гуглоте?

gds 20.03.2013 17:25

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

coq, cs, fp
gds 20.03.2013 15:22

"
Rc43: What does name of Agda mean?
olahol_: Agda the chicken, swedish floksong
"
Я всегда знал, что Coq — строго над Agda.

coq
gds 18.03.2013 11:44

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

coq, cs, fp, it, ocaml
gds 11.02.2013 18:03

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

coq, cs, it
iLeamare 03.12.2012 12:56

http://www.sendspace.com/file/4vtin4
Запись диалога знакомого в техподдержке с клиентом.

gds 05.11.2012 19:17

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

gds 12.06.2012 08:47

$ hg remove ErrorMonad.v StateMonad.v Monads.v Exceptions.v
до свиданья, наш ласковый мишка!11111

gds 02.06.2012 16:17

законтачился о монадные трансформеры, реализовав их (заодно манатки, заодно do-нотацию, заодно доказательства законов монад и трансформеров) в coq.

Fixpoint test1 (lst : list nat)
: idents_state Res MRes (list (nat * S.string))
:=
match lst with
| nil => ret nil
| cons h t =>
match h with
| 0 => lift (throw _ ... more →

coq
gds 01.06.2012 12:01

In the Soviet Coq, the monad transformer writes You!

gds 26.03.2012 01:20

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

gds 24.03.2012 18:06

I heard Coq like types, so we put type in your type so you can type your types while you are typing your types.

и больше ничего не могу сказать про текущие дела :)

coq
gds 16.03.2012 03:36

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

coq, cs
gds 12.03.2012 15:56

true <> false
Неожиданно? Однако, это так.
Эта шокирующая истина теперь конструктивно доказана: http://gds.livejournal.com/63887.html

gds 11.03.2012 12:55

http://gds.livejournal.com/63527.html — как обычно, интересуют каменты там либо тут. (не нравится щёлкать на ссылку — не щёлкайте, но копипастить ту простыню сюда я не буду.)

*coq is used by:

gds

gds