#coq:
(2012-04-24 20:40:40) apfelmus вышел из комнаты (quit: Quit: (λx.xx)(λx.xx)).
спрашивал в камлочятике, но спрошу и тут.
У кого-нибудь есть желание и возможность совместно поработать над типизированной императивщиной для atmega-подобных мелочей в рамках coq? Нужен в том числе опыт писания под эти или подобные мелкие процессоры. (если не знаете coq, но владеете функциональщиной — заодно ... more →
продолжение изложения основ теории категорий в понятном виде: http://thedeemon.livejournal.com/47570.h...
"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]
В одном из постов @beardog говорит "тяжело быть идиотом". Не знаю, идиот ли он, но я в этом и сомневаюсь, и считаю это совершенно не важным для текущего поста.
Потому что у меня опять параллели с языками программирования. (кто про что, а я опять про это говно.)
Я считаю, что идиотом быть просто, только последствия ... more →
сейчас наткнулся на подобную штуку, и немного генерализирую.
при написании веб-сервера на coq обнаружим, что рекурсивная функция, читающая http-заголовки, внезапно потребует доказательства завершимости. По идее, оно должно включить в себя конечность числа символов в прочитанных заголовках, либо конечность как числа ... more →
к моему посту #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 →
ааа, убейте меня, иначе я всё забрызгаю тут1111
@default631">http://flint.cs.yale.edu/cs428/coq/doc/R...
СУТЬ:
У вас есть индуктивный тип данных для представления вашего игрушечного AST, специфичного для вашей предметной области.
У вас есть функция, преобразующая _ваши_ значения из AST в ... more →
coq / ocaml = ocaml / c
крыша едет точно так же, как 10 лет назад от изучения функциональщины.
кстати, по "coq "program framework"" (собственно для написания кода, а не для доказательства) ищется слишком мало всего. Понятно, что фишка новая, но где про неё читать — ума не приложу. Есть идейки?
gadt'ы — только для typed [e]dsl evaluation
dependent types — только для проверки границ массивов
дискасс блеять.
вопрос про пользу зависимых типов: http://gds.livejournal.com/63409.html — покаментите, если есть мнение. (тут или там — пофиг.)
Как-то мне попалась в руки хорошая папира, хоть и от microsoft research, про "eventually consistent transactions": http://research.microsoft.com/pubs/15763...
И довольно удачно, потому что в работе подобное пригодится, вероятно.
И вот, дошли руки прочитать. Отзыв писал другому человеку, но ... more →
Тёплые ламповые^U Холодные шестерёнковые аналоговые компьютеры:
http://www.eugeneleeslover.com/VIDEOS/fi...
http://www.eugeneleeslover.com/VIDEOS/fi...
подумалась тривиальщина, по цепочке размышлений "бит → пол-бита".
по идее, пол-бита — это знание какого-либо факта с вероятностью 1/sqrt(2).
а есть ли какие-нибудь другие полезные штуки от представления вероятностей в битах, кроме всяких там шеннона и арифметического сжатия?
Кто (возможно) будет на *17th Estonian Winter School in Computer Science (EWSCS)* ?
http://cs.ioc.ee/ewscs/2012/
О, вот это и правда охуенчик:
http://james-iry.blogspot.com/2009/05/br...
Кто-то тут это постил, но я уже проебал тред, чтобы рекомендовать. Да мне и похуй как-то :3
Внезапно, квантовые компьютеры говно. С вероятностью 0 (почти всегда) они не ускоряют классические алгоритмы; а машина Тьюринга может симулировать полиномиальные по времени квантовые алгоритмы с использованием полиномиальной памяти.
И даже квантовая угроза этим вашим RSA не страшна. Есть куча устойчивых ... more →
Подскажите, пожалуйста, где почитать про алгоритмы для стандартной Линдоновской факторизации (standard Lyndon factorization) строк? Некий Jean-Pierre Duval опубликовал в 1983 и 1988 годах соответствующие труды, но их нигде не дают посмотреть — требуют денежку.
@jtootf: *programming *cs
http://www.ai-class.com/ http://www.db-class.org/ http://www.ml-class.org/ — эксперимент в области распределённого образования: три курса Стэнфорда, на которые можно записаться из (потенциально) любой точки мира. в отличие от обычных видеолекций, здесь предполагается обратная связь со ... more →
Пстач, я не говорил здесь сто раз про то, что буду что-то ботать летом, но мне всё равно нужна твоя помощь в составлении учебного плана на лето.
Собственно, все предметы в сабже, но всё же уточню.
Интересуют задачники, учебники, методички и готовые учебные планы.
Вообще, я скорее всего возьму учебный план у МФТИ ... more →
gds
ulidtko
4da
238328
Minoru
hedgehog
folex
Ky6uk
MPogoda
Elemir
utros
Marisa
XonX
add comment