Вообще увлекательнейший раздел, но хотелось бы приобщиться к нему без аксиоматически-алгебраистической целлюлозы.
Нет ли по вашему опыту учебника, который бы следовал духу арнольдовского (конструктивного и экспериментального) изложения, в простивовес душным алгебраистам?
Поищите работы Д. Скотта.
Автора широкоизвестного и популярного уточнения “смысла” бестипового лямбда-исчисления.
Некоторые его работы по этой теме очень неформально и живо написаны. Как, например, эта:
Скотт Д. Теория решеток, типы данных и семантика.
В сборнике: Данные в языках программирования.
М.: Мир, 1982, cc. 25 — 53.Начало этой статьи можно посмотреть здесь:
http://www.px-pict.com/preprints/Lambda/1.html