Типы в языках программирования, 5 курс, 2 семестр, 2016/17 — различия между версиями
Материал из SEWiki
(→Ссылки) |
(→Ссылки) |
||
| Строка 31: | Строка 31: | ||
* [http://oxij.org/note/BrutalDepTypes/ J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda] | * [http://oxij.org/note/BrutalDepTypes/ J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda] | ||
* [https://pdfs.semanticscholar.org/fec6/b29569eac1a340990bb07e90355efd2434ec.pdf E Meijer, M. Fokkinga, R. Paterson - Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire] | * [https://pdfs.semanticscholar.org/fec6/b29569eac1a340990bb07e90355efd2434ec.pdf E Meijer, M. Fokkinga, R. Paterson - Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire] | ||
| + | * [http://www.strictlypositive.org/diff.pdf C. McBride - The Derivative of a Regular Type is its Type of One-Hole Contexts] | ||
Версия 23:08, 24 апреля 2017
Преподаватель -- Елагин Кирилл
Лекции
Лекция 2. Простое типизированное лямбдя-исчисление
Лекция 4. АТД и рекурсивные типы
Практика
Ссылки
- Б. Пирс - Типы в языках программирования
- M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism
- J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda
- E Meijer, M. Fokkinga, R. Paterson - Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire
- C. McBride - The Derivative of a Regular Type is its Type of One-Hole Contexts
