$B65M\3XIt9-0h2J3X2J(B $B309q8lO@J89VFI(B I$B!&(BIII (2001$BG/EYE_3X4|(B)

$B%a%s%P!<(B

$BC4Ev(B
$B8^==Mr=_(B
$B;22C$B>.ED86Bg(B
$B2OFb0lN;(B
$B:4F#6)9d(B
$BI{ED=S2p(B
$B;fL>E/@8(B
$B;3K\FF(B
$B@>B$B6b;RCNE,(B
$B?e8}BgCO(B
$BGp86@h@8(B
$BEDCf@h@8(B
$B6L0f@h@8(B

$B%9%1%8%e!<%k(B

$BF|;~(B$B>l=j(B$BC4Ev
11/8(Thu.), 14:40-15$B9f4[(B405B$B8^==Mr(B(1$B>O(B)
11/15(Thu.), 14:40-15$B9f4[(B 106$BI{ED(B(3$B>O(B)
11/22(Thu.), 18:00-15$B9f4[(B 106$B;fL>(B(5$B>OA0H>(B)
11/29(Thu.), 14:40-15$B9f4[(B 405B$B;3K\(B(5$B>O8eH>(B)
12/6(Thu.), 14:40- 15$B9f4[(B 405B$B:4F#!$2OFb(B(8$B>O(B)
12/13(Thu.), 14:40- 15$B9f4[(B 405B$B:4F#!$2OFb(B(9$B>O(B)
12/20(Thu.), 14:40- 15$B9f4[(B 405B$B>.ED86!$2OFb(B(11$B>OA0H>(B)
1/10(Thu.), 14:40- 15$B9f4[(B 405B$B>.ED86!$2OFb(B(11$B>O8eH>(B)
1/24(Thu.), 14:40-15$B9f4[(B 405B$B:4F#!$I{ED(B(13$B>OA0H>(B)
1/31(Thu.), 14:40-15$B9f4[(B 405B$B:4F#!$I{ED(B(13$B>O8eH>(B)
2/7(Thu.), 14:40-15$B9f4[(B 405B$B>.ED86!$@>B<(B(15$B>O(B)
2/14(Thu.), 14:40-15$B9f4[(B 405B$B;fL>!$;3K\(B(18$B>O(B)

$B652J=q(B

Benjamin C. Pierce, Types and Programming Languages, ISBN 0262162091, MIT Press, 2002. ($BL$=PHG$N$?$a869F$rG[I[$7$^$9!%(B amazon.com $B$G(B 60$)

$BL\ ()$B$G0O$^$l$?>O$O!$>JN,M=Dj$G$9!%$^$?!$;~4VE*$K87$7$$$N$G(B $B:G=*>O$^$GE~C#$9$kM=Dj$b$"$j$^$;$s!%(B
  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) $