спец курс в ПОМИ [OT: Fwd: Ответ на ваш комментарий...]
Yakov ZAYTSEV
http://logic.pdmi.ras.ru/~infclub/
Есть идея попробовать выклянчить (короткий?) курс по, скажем, Мартин-Лефу у Шанина Н.А.
Цель - въехать (быстро войти в курс дела) в работу по Agda2, чтобы исчезли "страхи", с этой системой связанные ;-)
Кое-какие детали (в ходе обсуждения у меня в ЖЖ) см. ниже
Господа, высказывайтесь, что думаете по этому поводу!
From: weissefly - Комментарий в ЖЖ <lj_n...@livejournal.com>
Date: 2009/10/28
Subject: Ответ на ваш комментарий...
To: iak...@gmail.com
| Пользователь weissefly (weissefly) ответил на комментарий, оставленный вами к вашей записи в Живом Журнале. Комментарий, на который был получен ответ: |
ну, вообще-то если набралось бы хотя б 7..10 слушателей, то, думаю, реально это вполне, читают спец курсы, приходит и 6 человек.. (сам сидел на таком :-)Ответ был таким:
не знаю как там и что делается, но я бы с радостью заплатил бы за такой курс
вы бы могли в своей тусовке разнюхать про желающих?
если уж выходить на Шанина, то я бы составил программку, что-то вроде crash course in proof theory в разрезе теории типов и теории Мартина-Лефа (и может быть calculus of constructions), то есть так, чтобы после курса пропал "страх" и можно было смело работать (писать программы!) в Agda/Coq
тусовки особой у меня нет, но попробую кого-нибудь потыкать палочкой. предложите в spbHUG, там наиболее вероятно.
Alex Ott
лекций в интернет
Yakov ZAYTSEV at "Wed, 28 Oct 2009 15:52:32 +0300" wrote:
YZ> При ПОМИ есть comuter science клуб, в котором читаются разные лекции, напр., по теории сложности.
YZ> http://logic.pdmi.ras.ru/~infclub/
YZ> Есть идея попробовать выклянчить (короткий?) курс по, скажем, Мартин-Лефу у Шанина Н.А.
YZ> Цель - въехать (быстро войти в курс дела) в работу по Agda2, чтобы исчезли "страхи", с этой системой связанные ;-)
YZ> Кое-какие детали (в ходе обсуждения у меня в ЖЖ) см. ниже
YZ> Господа, высказывайтесь, что думаете по этому поводу!
YZ> ---------- Forwarded message ----------
YZ> From: weissefly - Комментарий в ЖЖ <lj_n...@livejournal.com>
YZ> Date: 2009/10/28
YZ> Subject: Ответ на ваш комментарий...
YZ> To: iak...@gmail.com
YZ> Пользователь weissefly (weissefly) ответил на комментарий, оставленный вами к вашей записи в Живом Журнале. Комментарий, на который был получен
YZ> ответ:
YZ> ну, вообще-то если набралось бы хотя б 7..10 слушателей, то, думаю, реально это вполне, читают спец курсы, приходит и 6 человек.. (сам
YZ> сидел на таком :-)
YZ>
YZ> не знаю как там и что делается, но я бы с радостью заплатил бы за такой курс
YZ>
YZ> вы бы могли в своей тусовке разнюхать про желающих?
YZ>
YZ> если уж выходить на Шанина, то я бы составил программку, что-то вроде crash course in proof theory в разрезе теории типов и теории
YZ> Мартина-Лефа (и может быть calculus of constructions), то есть так, чтобы после курса пропал "страх" и можно было смело работать (писать
YZ> программы!) в Agda/Coq
YZ> Ответ был таким:
YZ> тусовки особой у меня нет, но попробую кого-нибудь потыкать палочкой. предложите в spbHUG, там наиболее вероятно.
YZ>
--
With best wishes, Alex Ott, MBA
http://alexott.blogspot.com/ http://xtalk.msk.su/~ott/
http://alexott-ru.blogspot.com/
Yakov ZAYTSEV
было б грех :-)
2009/10/28 Alex Ott <ale...@gmail.com>:
--
Best wishes,
Y
Yakov ZAYTSEV
заранее, спасибо!
2009/10/28 Yakov ZAYTSEV <iak...@gmail.com>:
--
Best wishes,
Y
Denis Moskvin
Vladimir Sorokin
Только возникают более конкретные вопросы. Где? Когда? Длительность? Время начала? Требуемый базовый уровень знаний?
При ПОМИ есть comuter science клуб, в котором читаются разные лекции, напр., по теории сложности.
Yakov ZAYTSEV
причем оценить не толпу зевак, а из тесного т.с. круга тех, кто хотя б слыхал эти слова :-)
когда наберется хотя б 7..8 человек, я попытаюсь договариваться, это дело непростое ведь
--
Best wishes,
Y
Stanislav Serebryakov
On 10/28/09, Yakov ZAYTSEV <iak...@gmail.com> wrote:
> При ПОМИ есть comuter science клуб, в котором читаются разные лекции, напр.,
> по теории сложности.
>
> http://logic.pdmi.ras.ru/~infclub/
>
> Есть идея попробовать выклянчить (короткий?) курс по, скажем, Мартин-Лефу у
> Шанина Н.А.
>
> Цель - въехать (быстро войти в курс дела) в работу по Agda2, чтобы исчезли
> "страхи", с этой системой связанные ;-)
>
> Кое-какие детали (в ходе обсуждения у меня в ЖЖ) см. ниже
>
> Господа, высказывайтесь, что думаете по этому поводу!
>
> ---------- Forwarded message ----------
> From: weissefly - Комментарий в ЖЖ <lj_n...@livejournal.com>
> Date: 2009/10/28
> Subject: Ответ на ваш комментарий...
> To: iak...@gmail.com
>
>
> Пользователь weissefly (weissefly
> <http://weissefly.livejournal.com/profile>)
> ответил на комментарий, оставленный вами к вашей записи в Живом
> Журнале<http://iakovz.livejournal.com/140338.html>.
> Комментарий, на который был получен ответ:
>
> ну, вообще-то если набралось бы хотя б 7..10 слушателей, то, думаю, реально
> это вполне, читают спец курсы, приходит и 6 человек.. (сам сидел на таком
> :-)
>
> не знаю как там и что делается, но я бы с радостью заплатил бы за такой курс
>
> вы бы могли в своей тусовке разнюхать про желающих?
>
> если уж выходить на Шанина, то я бы составил программку, что-то вроде crash
> course in proof theory в разрезе теории типов и теории Мартина-Лефа (и может
> быть calculus of constructions), то есть так, чтобы после курса пропал
> "страх" и можно было смело работать (писать программы!) в Agda/Coq
>
> Ответ был таким:
>
> тусовки особой у меня нет, но попробую кого-нибудь потыкать палочкой.
> предложите в spbHUG, там наиболее вероятно.
>
> >
>
--
BR,
Stanislav `Cfr` Serebryakov,
http://claimid.com/cfr.
,-""-.
/--. \ .-.-'`-~
| () ) |<_.-.
\--' / `~._ `~'
`-..-' `- hjw
Stanislav Serebryakov
Kosta Sokolov
К.
On 29 окт, 18:23, Stanislav Serebryakov <cfr....@gmail.com> wrote:
> Т.е. я бы тоже послушал ;)
>
> Stanislav `Cfr` Serebryakov,http://claimid.com/cfr.
Daniil Elovkov
Привет
Я бы тоже с большой вероятностью посетил такой курс.
Правильно я понимаю, что не студенты тоже могут приходить, т.е. вообще кто угодно?
Yakov ZAYTSEV wrote:
> При ПОМИ есть comuter science клуб, в котором читаются разные лекции,
> напр., по теории сложности.
>
> http://logic.pdmi.ras.ru/~infclub/
>
> Есть идея попробовать выклянчить (короткий?) курс по, скажем,
> Мартин-Лефу у Шанина Н.А.
>
> Цель - въехать (быстро войти в курс дела) в работу по Agda2, чтобы
> исчезли "страхи", с этой системой связанные ;-)
>
> Кое-какие детали (в ходе обсуждения у меня в ЖЖ) см. ниже
>
> Господа, высказывайтесь, что думаете по этому поводу!
>
--
Daniil Elovkov
weissefly
Yakov ZAYTSEV
2009/10/29 Daniil Elovkov <daniil....@googlemail.com>:
--
Best wishes,
Y
Yakov ZAYTSEV
Шанин очень старенький уже, так что с ним не получится пообщаться
зато есть другая возможность, я поговорил с организатором клуба
Computer Science Александром
в принципе, можно попробовать сформулировать курс (а, главное лектора
для курса, которого надо будет прилететь к нам в Питер)
сформулировать надо так, чтобы сначала заинтересовать Александра в его
(курса) продвижении у спонсоров, здесь надо учесть специфику клуба --
массовая т.с. аудитория и, соотв., достаточно "общие" тема курсов,
хотя тут можно сделать хак ;-)
так как желающих было около десятка, давайте вместе посочиняем, вдруг,
получится, и к нам прилетит напр Benjamin Pierce ;-)
ну, думаю, намек вы поняли.
я по началу подумал о (а) курсе typed lambda calculus как напр в
книжке Proof and Types
(б) "засунуть" зависимые типы я придумал пока под видом "верификации
программ", напр., с помощью того же Coq whatever
ну, как, есть идеи?
то есть, как мне сказал Александр, для начала, надо предложить ему
профессора (специалиста) в этой теме, которую он потенциально будет
читать, кандидатура должна быть авторитетная по теме.
дальше -- что за курс будет читаться.. как-то так.
PS
это обсуждение не надо выносить за HUG IMHO
2009/10/30 Yakov ZAYTSEV <iak...@gmail.com>:
--
Best wishes,
Y
Laughedelic
On 28 окт, 15:52, Yakov ZAYTSEV <iak...@gmail.com> wrote:
> При ПОМИ есть comuter science клуб, в котором читаются разные лекции, напр.,
> по теории сложности.
>
> http://logic.pdmi.ras.ru/~infclub/
>
> Есть идея попробовать выклянчить (короткий?) курс по, скажем, Мартин-Лефу у
> Шанина Н.А.
>
> Цель - въехать (быстро войти в курс дела) в работу по Agda2, чтобы исчезли
> "страхи", с этой системой связанные ;-)
>
> Кое-какие детали (в ходе обсуждения у меня в ЖЖ) см. ниже
>
> Господа, высказывайтесь, что думаете по этому поводу!
>
> ---------- Forwarded message ----------
> From: weissefly - Комментарий в ЖЖ <lj_not...@livejournal.com>
> Date: 2009/10/28
> Subject: Ответ на ваш комментарий...
> To: iak...@gmail.com
>
> Пользователь weissefly (weissefly <http://weissefly.livejournal.com/profile>)
> ответил на комментарий, оставленный вами к вашей записи в Живом
> Журнале<http://iakovz.livejournal.com/140338.html>.