?

Log in

No account? Create an account
Введения в Agda - Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Введения в Agda [Jan. 23rd, 2013|11:09 pm]
Программирование с зависимыми типами

ru_deptypes

[deni_ok]
[Tags|]

Пара хороших введений в Агду. Оставлю здесь, чтобы было куда ссылаться.

Peter Divianszky (Eötvös Loránd University, Department of General Computer Science)
https://people.inf.elte.hu/divip/AgdaTutorial/Index.html

Thorsten Altenkirch (School of Computer Science, the University of Nottingham)
http://www.cs.nott.ac.uk/~txa/g53cfr/
LinkReply

Comments:
[User Picture]From: ulysses4ever
2013-01-23 08:22 pm (UTC)
Название целой лекции “Agda vs Haskell” это посильнее… чего угодно!
(Reply) (Thread)
[User Picture]From: deni_ok
2013-01-23 08:50 pm (UTC)
Ну, вообще-то, название лекции "Error propagation in Agda". Хотя, да, она какая-то короткая. Но дальше там у Торстена вполне себе хорошее изложение.
(Reply) (Parent) (Thread)
From: dima_starosud
2013-01-23 09:50 pm (UTC)
Вот еще (http://publications.lib.chalmers.se/records/fulltext/146810.pdf).
Это правда далеко не туториал, но долгое время я не мог ничего найти поглубже по Агда почитать, а тут мы недавно задавались вопросами type decidability, и меня направили на эту литературку.

*оффтоп: я писал в это комюнити, но пост не появился, кому жаловаться?
(Reply) (Thread)
[User Picture]From: deni_ok
2013-01-23 09:54 pm (UTC)
thesz тут ответственный и отец-основатель в одном лице.
(Reply) (Parent) (Thread)
From: dima_starosud
2013-01-23 09:58 pm (UTC)
Больше спасибо:)
И раз вы здесь, можете из ru_lambda тоже помочь?
Я туда заявку подал на участие, жду уже дней 5.
(Reply) (Parent) (Thread)
[User Picture]From: deni_ok
2013-01-23 10:06 pm (UTC)
Ну там alexott в мэйнтейнерах. Ему можно на gmail написать, у него тот же ник там.
(Reply) (Parent) (Thread)
From: dima_starosud
2013-01-23 10:09 pm (UTC)
Большое спасибо!
(Reply) (Parent) (Thread)