Joachim Lambek、P.J. Scott

ここで出てきた

これや『圏論の歩き方』など、型付きラムダ計算とCCCと直観主義論理の関係を調べると頻繁に参照されている