г. Черевиченко. Ссылки по лямбда-исчислению, категорной логике, топосам, теориям типов и т.п.

Некоторые ссылки по лямбда-исчислению, категорной логике, топосам, теориям типов и т.п.

Последние несколько лет семинар "Эффективная вычислимость и неклассические логики" проявляет интерес к этой тематике. Георгий Черевиченко (george66 AT mail.ru) взял на себя труд по поиску и отбору полезных материалов, доступных в электронном виде. Им же составлены короткие комментарии, появившиеся в результате профессиональной обработки указанных ресурсов. Я благодарен Георгию за этот большой труд и любезное разрешение разместить его результаты в открытом доступе. V.Kru

Много книг по категорной логике, теории типов, топосам и т.п. В том числе толстая книга Якобса и несколько учебников по теории категорий http://community.livejournal.com/category_theory/2190.html
Доходчивое введение Гейверса в теорию типов http://www.cs.ru.nl/~herman/PUBS/IntroTT.pdf
Книга "Programming in Martin-Lof's Type Theory" http://www.cs.chalmers.se/Cs/Research/Logic/book/
Книга Саймона Томпсона "Type Theory and Functional Programming" http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
Три учебника по теории категорий: Barr, Wells "Toposes, Triples and Theories" http://www.cwru.edu/artsci/math/wells/pub/ttt.html , Asperti, Longo "Categories, Types and Structures" (для специалистов по computer science) http://www.di.ens.fr/~longo/download.html Adamek, Herrlich, Strecker "Abstract and Concrete Categories - The Joy of Cats" http://katmat.math.uni-bremen.de/acc/acc.pdf ,
книга Wesley Phoa "An introduction to fibrations, topos theory, the effective topos and modest sets" (Хорошая книга, но требует знания основ теории категорий.) http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208.
Страница Пола Тэйлора (Paul Taylor). Можно скачать книгу Жирара "Proofs and Types" (Тэйлор ее переводил с французкого). Также можно скачать макросы, позволяющие набирать в LATEX деревья выводов и категорные диаграммы. http://www.paultaylor.eu/
Диссертация Andrej Bauer "The Realisability Approach to Computable Analysis and Topology". Описана категория т.н. эквилогических пространств (топологическое пространство с заданным на нем отношением эквивалентности), эта категория оказывается декартово замкнутой! http://andrej.com/thesis
Ну и на википедию полезно заходить: http://en.wikipedia.org/wiki/Category:Mathematical_logic, http://en.wikipedia.org/wiki/Category:Logic_in_computer_science.