應用邏輯討論會系列 (XXIX) -- Lecture 2 on the Introduction to Categorical Logic
- 講者濱野正浩 博士 (中研院資訊所)
邀請人：廖純中 - 時間2016-06-17 (Fri.) 15:30 ~ 17:30
- 地點資訊所新館101演講廳
摘要
This tutorial starts with briefly introducing the category theory through fundamental theorems (Yoneda lemma and Freyd adjoint functor theorem) as well as through an essential notion (monads).
A relationship to logic is given between Cartesian closed category and typed lambda-calculus so that the category theory gives a mathematical substance to Curry-Howard isomorphism. Further investigation is given in terms of elementary toposes and their logic (e.g., Kripke-Joyal definition of truth).
In more concrete aspects, we model Gentzen style cut-elimination for proofs, --statically by denotational semantics and --dynamically by feedback in traced monoidal categories.