$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
- Introduction
- Mathematical Preliminaries
Part I: Untyped Systems
- Untyped Arithmetic Expressions
- (An ML Implementation of Arithmetic Expressions)
- The Untyped Lambda-Calculus
- (Nameless Representation of Terms)
- (An ML Implementation of the Lambda-Calculus)
Part II: Simple Types
- Typed Arithmetic Expressions
- Simply Typed Lambda-Calculus
- (An ML Implementation of Simple Types)
- Simple Extensions
- (Normalization)
- References
- (Exceptions)
Part III: Subtyping
- Subtyping
- Metatheory of Subtyping
- (An ML Implementation of Subtyping)
- Case Study: Imperative Objects
- Case Study: Featherweight Java
Part IV: Recursive Types
- Recursive Types
- (Metatheory of Recursive Types)
Part V: Polymorphism
- Type Reconstruction
- Universal Types
- Existential Types
- Bounded Quantification
- Case Study: Imperative Objects, Redux
- (Metatheory of Bounded Quantification)
Part VI: Higher-Order Systems
- Type Operators and Kinding
- Higher-Order Polymorphism
- Higher-Order Subtyping
- Polymorphic Update
- Case Study: Purely Functional Objects
|