「型システム入門」と「ソフトウェアの基礎」の対応


「型システム入門」(TaPL)と「ソフトウェアの基礎」(SF)の進行性と保存性の説明の対応

型なし算術式

TaPL 型なし算術式 p.28
SF SmallStep (strong_progress) 数値
SF SmallStep (strong_progress) Bool、if-then-else

型付き算術式

TaPL 型付き算術式 p.72 (8.3.3、8.3.2)、Bool、if-then-else、数値
SF Types Bool、if-then-else、数値

型付きラムダ式

TaPL 型付きラムダ式 p.80 (9.3.5、9.3.9)、Bool、if-then-else
SF Stlc Bool、if-then-else、(練習問題:数値、if0)

SF MoreStlc List、直積、直和、数値、if0、fix、let

SF Records レコード

参照

TaPL 参照 p.129 (13.5.7、13.5.3)、参照
SF References 数値、if0、参照

例外

TaPL 例外 p.134 (14.1.2 Progress)

部分型付け

SF Subtyping Bool、if-then-else、(練習問題:直積)
TaPL 部分型付け p.149 (15.3.7、15.3.5)、レコード

SF RecordSub レコード

それ以外

TaPL FJ p.204 (19.5.4、19.5.1)
TaPL 全称型 p.277 (23.5.2、23.5.1)
TaPL 有界量化 p.317 (26.4.15、26.4.13)
TaPL 高階多相 p.361 (30.3.16、30.3.14)