Летняя школа в г.Оксфорд 2015 — различия между версиями

Материал из Вики ИТ мехмата ЮФУ
Перейти к: навигация, поиск
(инициальный коммит, пока только карточки лекторов)
 
(→‎Содержание)
Строка 26: Строка 26:
 
* Certified CYK parsing of context-free languages, 2014, coauth. Firsov // ''Journal of Logical and Algebraic Methods in Programming'' 83 (5), pp. 459-468.
 
* Certified CYK parsing of context-free languages, 2014, coauth. Firsov // ''Journal of Logical and Algebraic Methods in Programming'' 83 (5), pp. 459-468.
  
−
=== Содержание ===  
+
=== Содержание ===
 +
 
 +
'''Лекция 1''' (введение): монады, отображения монад, дистрибутивные законы. Примеры: исключения, Читатель, Писатель, списки в ассортименте (в т. ч. непустые, свободные от повторений и т. п.), когда их действие можно переставлять.
 +
 
 +
'''Лекция 2''': контейнеры, монадические контейнеры.
 +
Контейнер задаётся парой ''S'': '''Set''', ''P'': ''S'' → '''Set'''. Интерпретация ''F''=[|''S'', ''P''|] контейнера действует в категорию ['''Set''', '''Set'''] эндофункторов категории множеств по правилу: ''FX'' = {''Ps'' → ''X''}_{''s'': ''S''}. Основной пример: список; ''S'' = Nat, ''Ps'' = [0, … ''s''), ''FX'' = {[0, … ''s'') → ''X''} (список элементов типа ''X'' длины ''s'' это функция из [0, … ''s'') в ''X''). Основной результат: интерпретация является полным вложением (полным унивалентным функтором, fully faithful functor).
 +
Монадический контейнер это уже не пара, как обычный контейнер, а шестёрка. Интерпретация в этом случае является не просто функтором, а монадой.
 +
 
 +
'''Лекция 3''': моноидальные функторы, комонады. Более естественное понятие ''направленного контейнера'' (5 ингридиентов) порождает комонады в качестве интерпретаций. Примеры направленных контейнеров: потоки (бесконечные коллекции, S = 1, P· = Nat), непустые списки.
  
 
== Встроенные предметно-ориентированные языки в Idris (Э. Брэди) ==  
 
== Встроенные предметно-ориентированные языки в Idris (Э. Брэди) ==  

Версия 15:47, 16 июля 2015

Библиотека колледжа Сэн Энн, в котором проводилась школа

Летняя школа в Оксфордском университете проходила с 6 по 10 июля 2015 года, лекции читались 4 и ¼ дня, по 4 лекции в день. Официальное название: Summer School on Generic and Effectful Programming (Летняя школа по обобщённому программированию и программированию с вычислительными эффектами).

Официальная точка входа к материалам школам расположена на сайте школы. Однако на всякий случай материалы продублированы (и местами дополнены заметками и релевантными статьями) в Дропбоксе.

Ниже приведён список курсов лекций с карточками лекторов и комментариями.

Контейнеры для эффектов и контекстов (Т. Уусталу)

Лектор

Тармо Уусталу

Место работы: Институт кибернетики Талиннского университета технологии.

Тема диссертации: Natural Deduction for Intuitionistic Least and Greatest Fixedpoint Logics, with an Application to Program Construction, 1998, Stockholm.

Основные публикации

  • Type-based termination of recursive definitions, 2004, coauth. Barthe, Frade, Giménez, Pinto // Mathematical Structures in Computer Science 14 (01), pp. 97-141. Cit. 95.
  • Primitive (Co) Recursion and Course-of-Value (Co) Iteration, Categorically, 1999, coauth. Vene // Informatica, Lith. Acad. Sci. 10 (1), pp. 5-26. Cit. 78.
  • Iteration and coiteration schemes for higher-order and nested datatypes, 2005, coauth. Abel, Matthes // Theoretical Computer Science 333 (1), pp. 3-66. Cit. 53.

Недавние публикации

  • Certified CYK parsing of context-free languages, 2014, coauth. Firsov // Journal of Logical and Algebraic Methods in Programming 83 (5), pp. 459-468.

Содержание

Лекция 1 (введение): монады, отображения монад, дистрибутивные законы. Примеры: исключения, Читатель, Писатель, списки в ассортименте (в т. ч. непустые, свободные от повторений и т. п.), когда их действие можно переставлять.

Лекция 2: контейнеры, монадические контейнеры. Контейнер задаётся парой S: Set, P: S → Set. Интерпретация F=[|S, P|] контейнера действует в категорию [Set, Set] эндофункторов категории множеств по правилу: FX = {Ps → X}_{s: S}. Основной пример: список; S = Nat, Ps = [0, … s), FX = {[0, … s) → X} (список элементов типа X длины s это функция из [0, … s) в X). Основной результат: интерпретация является полным вложением (полным унивалентным функтором, fully faithful functor). Монадический контейнер это уже не пара, как обычный контейнер, а шестёрка. Интерпретация в этом случае является не просто функтором, а монадой.

Лекция 3: моноидальные функторы, комонады. Более естественное понятие направленного контейнера (5 ингридиентов) порождает комонады в качестве интерпретаций. Примеры направленных контейнеров: потоки (бесконечные коллекции, S = 1, P· = Nat), непустые списки.

Встроенные предметно-ориентированные языки в Idris (Э. Брэди)

Лектор

Эдвин Брэди

Место работы: Университет Сэн Эндрюса, Великобритания.

Тема диссертации: Practical Implementation of a Dependently Typed Functional Programming Language, 2005, Durham U.

Основные публикации

  • Inductive families need not store their indices, 2004, coauth. McBride, McKinna // Types for proofs and programs, pp. 115-129. Cit. 73.
  • Idris, a general-purpose dependently typed programming language: Design and implementation, 2013 // Journal of Functional Programming 23 (05), pp. 552-593. Cit. 60.
  • IDRIS---: systems programming meets full dependent types, 2011 // Proceedings of the 5th ACM workshop on Programming languages meets program verification, pp. 43-54. Cit. 51.

Недавние публикации

  • Cross-platform Compilers for Functional Languages, 2015 // Under consideration for Trends in Functional Programming.
  • Resource-Dependent Algebraic Effects, 2015 // Trends in Functional Programming, pp. 18-33.

Содержание

Эффективное в худшем случае обобщённое функциональное программирование с массивами данными (Ф. Хенглейн)

Лектор

Фриц Хенглейн

Место работы: Университет Копенгагена, Дания.

Тема диссертации: Polymorphic Type Inference and Semi-Unification, 1989, Rutgers U.

Основные публикации

  • Type inference with polymorphic recursion, 1993 // ACM Transactions on Programming Languages and Systems 15 (2), pp. 253-289. Cit. 288.
  • Dynamic typing: Syntax and proof theory, 1994 // Science of Computer Programming 22 (3), pp. 197-230. Cit. 168.
  • Efficient type inference for higher-order binding-time analysis, 1991 // Functional Programming Languages and Computer Architecture, pp. 448-472. Cit. 153.

Недавние публикации

  • Domain-specific languages for enterprise systems, 2014 // Leveraging Applications of Formal Methods, Verification and Validation, pp. 73-95.
  • Optimally Streaming Greedy Regular Expression Parsing, 2014, coauth. Grathwohl, Rasmussen // Theoretical Aspects of Computing, pp. 224-240.

Содержание

Применение обобщенного программирования и программирования на уровне типов в Haskell (А. Лёх)

Лектор

Андрес Лёх

Место работы: компания Well-Typed.

Тема диссертации: Exploring Generic Haskell. 2004, Utrecht U.

Основные публикации

  • Type-indexed data types, 2002, coauth. Hinze, Jeuring // Mathematics of Program Construction, pp. 148-174. Cit. 118.
  • “Scrap Your Boilerplate” Reloaded, 2006, coauth. Hinze, Oliveira // Functional and Logic Programming, pp. 13-29. Cit. 77.
  • Generic H∀ SKELL, Specifically, 2003, coauth. Clarke // Generic Programming, pp. 21-47. Cit. 76.

Недавние публикации

  • The semantics of version control, 2014, coauth. Swierstra // Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, pp. 43-54.
  • Generic generic programming, 2014, coauth. Magalhaes // Practical Aspects of Declarative Languages, pp. 216-231.

Содержание

Ссылки

Типы данных типов данных (К. Макбрайд)

Лектор

Конор Макбрайд

Место работы: Университет Стрэтклайда, Шотландия.

Тема диссертации: Dependently Typed Functional Programs and theis Proofs, 1999, U. of Edinburg.

Основные публикации

  • The view from the left, 2004, coauth. McKinna // Journal of Functional Programming 14 (1), pp. 69-111. Cit. 335.
  • Applicative programming with effects, 2008, coauth. Paterson // Journal of functional programming 18 (01), pp. 1-13. Cit. 263.
  • Faking it Simulating dependent types in Haskell, 2002 // Journal of functional programming 12 (4-5), pp. 375-392. Cit. 119.

Недавние публикации

  • Indexed containers, 2015, coauth. Altenkirch, Ghani, Hancock, Morris // Journal of Functional Programming 25, e5.
  • Hasochism: the pleasure and pain of dependently typed Haskell programming, 2014, coauth. Lindley // ACM SIGPLAN Notices 48 (12), pp. 81-92.

Содержание

Метапрограммирование времени компиляции в информационном мире (Д. Сайм)

Лектор

Дон Сайм

Место работы: Microsoft Research в Кэмбридже, Великобритания.

Тема диссертации: ???, PhD studies in Cambridge U.

Основные публикации

  • Design and implementation of generics for the. net common language runtime, 2001, coauth. Kennedy // ACM SigPlan Notices 36 (5), pp. 1-12. Cit. 263.
  • Proving Java type soundness, 1999 // Formal Syntax and Semantics of Java, 83-pp. 118. Cit. 161.
  • Typing a multi-language intermediate code, 2001, coauth. Gordon // ACM SIGPLAN Notices 36 (3), pp. 248-260. Cit. 121.

Недавние публикации

  • F# Data: Making structured data first class citizens, 2015, coauth. Petricek, Guerra // Unpublished draft.
  • Expert F# 3.0, 2012, coauth. Granicz, A Cisternino // Apress.

Содержание

Источник — «http://it.mmcs.sfedu.ru/_wiki/index.php?title=Летняя_школа_в_г.Оксфорд_2015&oldid=6051»