対象とする聴衆のレベル（該当するレベルを記載してください。）

• Beginner: 分野の前提知識を必要としない

セッションのテーマ（該当するテーマを記載してください。なければ追加頂いて良いです）

• 理論
• 入門

セッションの概要

本セッションは、数理論理学を学ぶことによって型システム理論への入門が容易になると主張するものです。
発表者はかつて『型システム入門』の勉強会に参加していましたが、参加者の一部はプログラマではないにもかかわらず、ときに職業プログラマーである発表者よりも、深く内容を理解できていました。彼らは、数理論理学に深く通じているという点で共通していました。
なぜ数理論理学の知識が型システム理論の理解を助けるのでしょうか？それは、静的型付け言語における操作的意味論と型システムの関係が、論理学における意味論と証明体系の関係に対応するからだと発表者は考えています。つまり、論理学に詳しい彼らにとって、『型システム入門』の内容はとても馴染みのあるものだったのです。
そこで本発表では、『型システム入門』への入門を目論んでいる方々に向けて、あえて数理論理学を経由することを提案します。セッションは次のような内容を含みます。

• 論理学における意味論・証明体系の概要と、両者の関係
• 静的型付け言語における操作的意味論と型システムの概要と、両者の関係
• まとめとして、論理学と型システム理論の類似性