Типы в языках программирования, 5 курс, 2 семестр, 2016/17 — различия между версиями
Материал из SEWiki
(→Лекции) |
(→Ссылки) |
||
Строка 35: | Строка 35: | ||
* [http://starling.rinet.ru/~goga/tapl/tapl.pdf Б. Пирс - Типы в языках программирования] | * [http://starling.rinet.ru/~goga/tapl/tapl.pdf Б. Пирс - Типы в языках программирования] | ||
* [http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism] | * [http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism] | ||
+ | * [http://cs.swan.ac.uk/~cspt/DependentTypes.pdf D. Aspinall, M. Hofmann - Dependent Types] | ||
* [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] | ||
+ | * [http://cs.swan.ac.uk/~cspt/DependentTypes.pdf F. Pottier, D. Rémy - The Essence of ML Type Inference] | ||
* [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] | * [http://www.strictlypositive.org/diff.pdf C. McBride - The Derivative of a Regular Type is its Type of One-Hole Contexts] | ||
+ | * [https://mitpress.mit.edu/sites/default/files/titles/content/9780262162289_sch_0001.pdf D. Walker - Substructural Type Systems] |
Версия 05:01, 23 мая 2017
Преподаватель -- Елагин Кирилл
Лекции
Лекция 2. Простое типизированное лямбдя-исчисление
Лекция 4. АТД и рекурсивные типы
Лекция 8. Чистые системы типов
Лекция 12. Экзистенциальные типы
Лекция 13. Обзор: зипперы, типы-пересечения, субструктурные логики
Практика
Ссылки
- Б. Пирс - Типы в языках программирования
- M. H. Sørensen, P. Urzyczyn - Lectures on the Curry-Howard Isomorphism
- D. Aspinall, M. Hofmann - Dependent Types
- J. Malakhovski - Brutal [Meta]Introduction to Dependent Types in Agda
- F. Pottier, D. Rémy - The Essence of ML Type Inference
- 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
- D. Walker - Substructural Type Systems