OCaml (aka Objective Caml), а также прочие ML'и, F#, Coq, etc

ocaml@conference.jabber.ru

Четверг, 17 октября 2013< ^ >

Конфигурация комнаты

Участники комнаты

GMT+4
[00:10:02] tilarids вошёл(а) в комнату
[00:10:22] tilarids вышел(а) из комнаты: Machine going to sleep
[00:17:14] Kakadu вышел(а) из комнаты
[00:30:08] komar вышел(а) из комнаты: Replaced by new connection
[00:30:08] komar вошёл(а) в комнату
[01:16:58] tilarids вошёл(а) в комнату
[01:21:11] komar вышел(а) из комнаты: Replaced by new connection
[01:21:11] komar вошёл(а) в комнату
[02:09:17] tilarids вышел(а) из комнаты: Machine going to sleep
[02:20:00] tilarids вошёл(а) в комнату
[02:39:58] strobegen вышел(а) из комнаты
[03:12:29] komar вышел(а) из комнаты: Replaced by new connection
[03:12:29] komar вошёл(а) в комнату
[03:14:59] komar вышел(а) из комнаты: Replaced by new connection
[03:15:07] komar вошёл(а) в комнату
[03:18:09] komar вышел(а) из комнаты: Replaced by new connection
[03:18:09] komar вошёл(а) в комнату
[04:40:33] strobegen вошёл(а) в комнату
[05:13:11] tilarids вышел(а) из комнаты: Machine going to sleep
[05:25:33] komar вышел(а) из комнаты: Replaced by new connection
[05:25:33] komar вошёл(а) в комнату
[05:29:32] komar вышел(а) из комнаты: Replaced by new connection
[05:29:32] komar вошёл(а) в комнату
[05:50:49] f[x] вошёл(а) в комнату
[06:16:27] komar вышел(а) из комнаты: Replaced by new connection
[06:16:27] komar вошёл(а) в комнату
[06:48:52] komar вышел(а) из комнаты: Replaced by new connection
[06:48:52] komar вошёл(а) в комнату
[06:51:00] komar вышел(а) из комнаты: Replaced by new connection
[06:51:00] komar вошёл(а) в комнату
[07:33:42] olibjerd вошёл(а) в комнату
[08:32:17] olibjerd вышел(а) из комнаты
[09:26:15] komar вышел(а) из комнаты: Replaced by new connection
[09:26:15] komar вошёл(а) в комнату
[09:53:18] tilarids вошёл(а) в комнату
[10:02:27] f[x] вышел(а) из комнаты
[10:47:24] ermine вошёл(а) в комнату
[11:01:19] f[x] вошёл(а) в комнату
[11:09:27] f[x] вышел(а) из комнаты
[11:10:31] tilarids вышел(а) из комнаты: Machine going to sleep
[11:25:35] komar вышел(а) из комнаты: Replaced by new connection
[11:25:35] komar вошёл(а) в комнату
[11:40:49] f[x] вошёл(а) в комнату
[11:51:58] f[x] вышел(а) из комнаты
[11:56:30] Kakadu вошёл(а) в комнату
[12:00:39] komar вышел(а) из комнаты: Replaced by new connection
[12:00:39] komar вошёл(а) в комнату
[12:23:09] f[x] вошёл(а) в комнату
[12:25:50] strobegen вышел(а) из комнаты: Replaced by new connection
[12:25:51] strobegen вошёл(а) в комнату
[12:42:26] f[x] вышел(а) из комнаты
[12:45:09] komar вышел(а) из комнаты: Replaced by new connection
[12:45:09] komar вошёл(а) в комнату
[13:12:00] Typhon вошёл(а) в комнату
[13:37:31] f[x] вошёл(а) в комнату
[13:39:39] klapaucius вышел(а) из комнаты
[13:51:12] komar вышел(а) из комнаты: Replaced by new connection
[13:51:12] komar вошёл(а) в комнату
[13:56:46] klapaucius вошёл(а) в комнату
[14:17:52] komar вышел(а) из комнаты: Replaced by new connection
[14:17:53] komar вошёл(а) в комнату
[14:44:17] Zbroyar вошёл(а) в комнату
[14:52:04] f[x] вышел(а) из комнаты
[15:43:37] Zbroyar вышел(а) из комнаты
[16:07:23] <gds> может кому интересно будет (проект "симулятор многопоточного выполнения"): http://gds.psto.net/tgehhn
[16:38:06] <aleksey> а как же coq
[16:43:18] klapaucius вышел(а) из комнаты
[16:43:21] klapaucius вошёл(а) в комнату
[17:06:12] <gds> aleksey: с него и началось размышление. В конце концов, пришлось бы делать ровно такое же дерево перебора. А как иначе?
[17:07:11] komar вышел(а) из комнаты
[17:07:27] <aleksey> ну дерево часто поменьше можно сделать
[17:07:36] <aleksey> причём на порядки меньше
[17:08:34] komar вошёл(а) в комнату
[17:18:29] <gds> aleksey: возможно. Но вот у меня есть проблемки -- сложно сформулировать это дело в кококо. Если бы кто-нибудь помог с формализацией базовых вещей, я бы продолжил дальше.
[17:20:08] <aleksey> ну для каждого процеса есть последовательность действий, и между некоторыми этими действиями есть ограничения типа "B только после A"
[17:21:03] <aleksey> ну и в коке видимо просто надо сказать "для любой возможной последовательности где выполняются эти ограничения должен быть корректный результат"
[17:22:35] <gds> но перебором проще получить контрпример, в коке же потребуется доказывать exists x, ограничение на x -> False.
[17:27:11] <aleksey> зато перебирать меньше
[17:39:21] klapaucius вышел(а) из комнаты
[17:54:33] komar вышел(а) из комнаты: Replaced by new connection
[17:54:33] komar вошёл(а) в комнату
[18:09:26] Typhon вышел(а) из комнаты: Replaced by new connection
[18:09:36] Typhon вошёл(а) в комнату
[18:20:26] Zbroyar вошёл(а) в комнату
[18:25:18] Zbroyar вышел(а) из комнаты: Replaced by new connection
[18:25:21] Zbroyar вошёл(а) в комнату
[18:43:15] tilarids вошёл(а) в комнату
[18:50:14] Typhon вышел(а) из комнаты
[19:22:12] Zbroyar вышел(а) из комнаты
[19:38:55] olibjerd вошёл(а) в комнату
[19:44:56] Zbroyar вошёл(а) в комнату
[20:10:57] Zbroyar вышел(а) из комнаты
[20:23:43] olibjerd вышел(а) из комнаты
[20:25:33] tilarids вышел(а) из комнаты: Machine going to sleep
[20:49:09] Zbroyar вошёл(а) в комнату
[20:50:13] Zbroyar вышел(а) из комнаты
[21:21:43] Kakadu вышел(а) из комнаты
[22:06:34] Kakadu вошёл(а) в комнату
[22:45:15] tilarids вошёл(а) в комнату
[22:51:56] ermine вышел(а) из комнаты
[23:07:12] ermine вошёл(а) в комнату
[23:13:25] ermine вышел(а) из комнаты