計算論理学   [ GB21404 ] Computational Logic
対象：3・4学年	開設学期：秋AB	曜日・時限：木5・6	単位数：2単位
担当教員：亀山幸義, 海野広志

概要

多くの現代的プログラム言語は，強力な型システムを持つことによりデータ構造や制御構造の抽象化を果たし，プログラムの誤りを減らしたり，可読性を高めることに役立っている．本講義では，型システムの理論的背景を知るため，型つきラムダ計算に基づいたプログラム言語の基礎理論を学ぶ．プログラム言語の構文と意味の厳密な定義方法，型システム，計算規則などについて学ぶ．また，型つきラムダ計算に対応する直観主義論理の体系を取り上げ，これら２つの体系が本質的に等価であること，すなわち，証明とプログラムが同一視できることを学ぶ．これらを通じて形式的体系とは何かを理解し，形式的対象の操作が計算機で実行可能なことを学ぶ．授業の中でソフトウェアを用いた演習を行う．

学習・教育目標

プログラム言語と論理体系を題材にして，形式体系の取り扱いを理解する．また，プログラム言語における型システムの役割，理論，応用を理解する．

キーワード

形式体系，構文と意味，命題論理，ラムダ計算，型システム，証明とプログラム，プログラム検証．

Keywords

Formal System, Syntax and Semantics, Propositional Logic, Lambda Calculus, Type System, Proofs and Programs, Program Verification.

時間割

週	講義内容/理解すべき項目
第１週	導入: ラムダ計算，形式体系，構文論と意味論
第２週	計算の論理： 命題論理、直観主義論理，導出
第３−７週	型付きラムダ計算: 項と型，計算，性質，型検査と型推論、多相型、進んだ話題
第８−９週	依存型とリファインメント型、プログラム検証
第１０週	授業のまとめ

教材

講義資料は，この授業のホームページ等を通じて公開する．

参考書籍

プログラムの基礎理論（佐藤雅彦・桜井貴文共著，岩 波書店）
ソフトウェア科学のための論理学（萩谷昌己著，岩波書 店）
Benjamine C. Pierce,"Types and Programming　 Languages", MIT Press, 2002.

予備知識・前提条件

「論理と形式化」もしくは形式体系・論理の基礎的事項

成績評価

講義への出席を前提として，演習５０％，期末試験５０％により評価する．

教員メールアドレス

亀山：　kam [at] cs tsukuba ac jp
海野：　uhiro [at] cs tsukuba ac jp

TF・TA

薄井： usui [at] logic cs tsukuba ac jp

講義のWebページ

http://logic.cs.tsukuba.ac.jp/~kam/complogic/

オフィスアワー

初回の講義で指定する．