Теория типов и изоморфизм Карри-Ховарда: Глубокая гармония между Суждениями=Типами и Доказательствами=Программами
