教養学部広域科学科 外国語論文講読 I・III (2001年度冬学期)

メンバー

担当
五十嵐淳
参加者
小田原大
河内一了
佐藤匡剛
副田俊介
紙名哲生
山本篤
西村大介
金子知適
水口大地
柏原先生
田中先生
玉井先生

スケジュール

日時場所担当者・担当個所
11/8(Thu.), 14:40-15号館405B五十嵐(1章)
11/15(Thu.), 14:40-15号館 106副田(3章)
11/22(Thu.), 18:00-15号館 106紙名(5章前半)
11/29(Thu.), 14:40-15号館 405B山本(5章後半)
12/6(Thu.), 14:40- 15号館 405B佐藤,河内(8章)
12/13(Thu.), 14:40- 15号館 405B佐藤,河内(9章)
12/20(Thu.), 14:40- 15号館 405B小田原,河内(11章前半)
1/10(Thu.), 14:40- 15号館 405B小田原,河内(11章後半)
1/24(Thu.), 14:40-15号館 405B佐藤,副田(13章前半)
1/31(Thu.), 14:40-15号館 405B佐藤,副田(13章後半)
2/7(Thu.), 14:40-15号館 405B小田原,西村(15章)
2/14(Thu.), 14:40-15号館 405B紙名,山本(18章)

教科書

Benjamin C. Pierce, Types and Programming Languages, ISBN 0262162091, MIT Press, 2002. (未出版のため原稿を配布します. amazon.com で 60$)

目次

()で囲まれた章は,省略予定です.また,時間的に厳しいので 最終章まで到達する予定もありません.
  1. Introduction
  2. Mathematical Preliminaries

Part I: Untyped Systems

  1. Untyped Arithmetic Expressions
  2. (An ML Implementation of Arithmetic Expressions)
  3. The Untyped Lambda-Calculus
  4. (Nameless Representation of Terms)
  5. (An ML Implementation of the Lambda-Calculus)

Part II: Simple Types

  1. Typed Arithmetic Expressions
  2. Simply Typed Lambda-Calculus
  3. (An ML Implementation of Simple Types)
  4. Simple Extensions
  5. (Normalization)
  6. References
  7. (Exceptions)

Part III: Subtyping

  1. Subtyping
  2. Metatheory of Subtyping
  3. (An ML Implementation of Subtyping)
  4. Case Study: Imperative Objects
  5. Case Study: Featherweight Java

Part IV: Recursive Types

  1. Recursive Types
  2. (Metatheory of Recursive Types)

Part V: Polymorphism

  1. Type Reconstruction
  2. Universal Types
  3. Existential Types
  4. Bounded Quantification
  5. Case Study: Imperative Objects, Redux
  6. (Metatheory of Bounded Quantification)

Part VI: Higher-Order Systems

  1. Type Operators and Kinding
  2. Higher-Order Polymorphism
  3. Higher-Order Subtyping
  4. Polymorphic Update
  5. Case Study: Purely Functional Objects

igarashi@graco.c.u-tokyo.ac.jp
Last update on $Date: 2002-04-25 16:00:38 +0900 (, 25 4 2002) $