中央研究院 資訊科學研究所

活動訊息

友善列印

列印可使用瀏覽器提供的(Ctrl+P)功能

應用邏輯討論會系列 (XXVIII) -- Lecture 1 on the Introduction to Categorical Logic

:::

應用邏輯討論會系列 (XXVIII) -- Lecture 1 on the Introduction to Categorical Logic

  • 講者濱野正浩 博士 (中央研究院資訊科學研究所客座研究員)
    邀請人:廖純中
  • 時間2016-05-27 (Fri.) 15:30 ~ 17:30
  • 地點資訊所新館106演講廳
摘要

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.