Летняя школа в г.Оксфорд 2015 — различия между версиями
Ulysses (обсуждение | вклад) (инициальный коммит, пока только карточки лекторов) |
(нет различий)
|
Версия 13:16, 16 июля 2015
Летняя школа в Оксфордском университете проходила с 6 по 10 июля 2015 года, лекции читались 4 и ¼ дня, по 4 лекции в день. Официальное название: Summer School on Generic and Effectful Programming (Летняя школа по обобщённому программированию и программированию с вычислительными эффектами).
Официальная точка входа к материалам школам расположена на сайте школы. Однако на всякий случай материалы продублированы (и местами дополнены заметками и релевантными статьями) в Дропбоксе.
Ниже приведён список курсов лекций с карточками лекторов и комментариями.
Содержание
- 1 Контейнеры для эффектов и контекстов (Т. Уусталу)
- 2 Встроенные предметно-ориентированные языки в Idris (Э. Брэди)
- 3 Эффективное в худшем случае обобщённое функциональное программирование с массивами данными (Ф. Хенглейн)
- 4 Применение обобщенного программирования и программирования на уровне типов в Haskell (А. Лёх)
- 5 Типы данных типов данных (К. Макбрайд)
- 6 Метапрограммирование времени компиляции в информационном мире (Д. Сайм)
Контейнеры для эффектов и контекстов (Т. Уусталу)
Лектор
Место работы: Институт кибернетики Талиннского университета технологии.
Тема диссертации: 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.
Содержание
Встроенные предметно-ориентированные языки в 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.