推論規則〈inference rule〉と型つけ規則〈typing rule〉の両方を含むシステムで使いやすいものがないかな、と探していました。僕が思う“使いやすい”とは： 意味論〈セマンティクス〉はハイパードクトリン。 カリー／ハワード／ランベック対応と相性がよい。…