С. Исакова (Академический Университет)

Типизированное лямбда-исчисление

В докладе будет рассказано, что такое изоморфизм Карри-Говарда. Это прямое
соответствие между формулами и доказательствами в интуиционистской логике и
программами (термами) и их типами в типизированном лямбда-исчислении. Будут
введены все необходимые для этого определения и понятия. В завершении будет
показано, как задача QBF сводится к задаче построения терма с заданным
типом.