Здесь лежит по-моему интересная лекция с Google Talks (из серии Advanced Topics in Programming Languages Series, Mirrorer приводил не так давно другую лекцию из этой серии

Автор: Mirrorer
Дата: 28.03.07

, но эта много "вменяемей" на мой взгляд, чем та). Тема очень пересекается с лекцией Вадлера

Автор: Курилка
Дата: 05.05.07

: система Хиндли-Милнера, изоморфизмы Карри-Говарда, Жирарда-Рейнольдса. Довольно интересна идея "вывода кода" как изоморфизма выводу типов, только не знаю, имеет ли это реальное практическое применение.