Типы в языках программирования, 5 курс, 2 семестр, 2016/17 — различия между версиями
Материал из SEWiki
(→Лекции) |
(→Ссылки) |
||
| (не показано 10 промежуточных версий этого же участника) | |||
| Строка 3: | Строка 3: | ||
== Лекции == | == Лекции == | ||
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/01-syntax-and-semantics.html Лекция 1. Синтаксис и семантики] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/02-stlc.html Лекция 2. Простое типизированное лямбдя-исчисление] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/03-normalization-and-pfc.html Лекция 3. Нормализация] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/04-ADTs-and-mu.html Лекция 4. АТД и рекурсивные типы] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/05-System-F.html Лекция 5. System F] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/06-System-F-omega.html Лекция 6. System Fω] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/07-dependent.html Лекция 7. Зависимые типы] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/08-PTS.html Лекция 8. Чистые системы типов] |
| − | [https://kir.elagin.me/edu/types/ | + | [https://kir.elagin.me/edu/types/09-type-checking-and-co.html Лекция 9. Проверка типов] |
[https://kir.elagin.me/edu/types/10-catamorphisms.html Лекция 10. Катаморфизмы] | [https://kir.elagin.me/edu/types/10-catamorphisms.html Лекция 10. Катаморфизмы] | ||
| + | |||
| + | [https://kir.elagin.me/edu/types/11-subtyping.html Лекция 11. Подтипы] | ||
| + | |||
| + | [https://kir.elagin.me/edu/types/12-existential.html Лекция 12. Экзистенциальные типы] | ||
| + | |||
| + | [https://kir.elagin.me/edu/types/13-misc.html Лекция 13. Обзор: зипперы, типы-пересечения, субструктурные системы типов] | ||
== Практика == | == Практика == | ||
| Строка 27: | Строка 33: | ||
== Ссылки == | == Ссылки == | ||
| − | * [http:// | + | *[http://port70.net/~nsz/articles/book/pierce_types_and_programming_languages_2002.pdf B. C. Pierce - Types and Programming Languages] ([http://newstar.rinet.ru/~goga/tapl/tapl.pdf RU]) |
| + | |||
* [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://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf H. P. Barendregt - Lambda Calculi with Types] | ||
| + | |||
| + | *[http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf H. Geuvers - Introduction to Type Theory] | ||
| + | |||
| + | * [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] | ||
| + | |||
| + | * [https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf P. Wadler - Theorems for Free!] | ||
| + | |||
| + | * [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] | ||
| + | |||
| + | * [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] | ||
| + | |||
| + | * [http://mit.spbau.ru/sewiki/index.php/Типы_в_языках_программирования_6_2015 Д. Н. Москвин - Типы в языках программирования, 2015 год] | ||
| + | |||
| + | * [http://compsciclub.ru/courses/systemsoftypedlambdacalculi/2011-spring/ Д. Н. Москвин - Системы типизации лямбда-исчисления, 2011 год] | ||
Текущая версия на 05:23, 2 июля 2017
Преподаватель -- Елагин Кирилл
Лекции
Лекция 1. Синтаксис и семантики
Лекция 2. Простое типизированное лямбдя-исчисление
Лекция 4. АТД и рекурсивные типы
Лекция 8. Чистые системы типов
Лекция 12. Экзистенциальные типы
Лекция 13. Обзор: зипперы, типы-пересечения, субструктурные системы типов
