Декартово замкнутые категории, логика и лямбда-исчисление

Доклад будет опираться на 6 главу текста Introduction to Categories and Categorical Logic (Abramsky, Tzevelekos). Сперва мы посмотрим на декартово замкнутую категорию как на модель фрагмента пропозициональной логики. Затем будут даны основные понятия, касающиеся простого типизированного лямбда-исчисления (STLC). Мы рассмотрим семантику STLC на произвольной декартово замкнутой категории и покажем её корректность. После этого будет построена категория $C_\lambda$, которая является корректной и полной моделью STLC.