List of Figures

---

Preface

Figure P-1: Chapter Dependencies

Figure P-2: Sample Syllabus for an Advanced Graduate Course

Chapter 1: Introduction

Figure 1-1: Capsule History of Types in Computer Science and Logic

Chapter 3: Untyped Arithmetic Expressions

Figure 3-1: Booleans (B)

Figure 3-2: Arithmetic Expressions (NB)

Chapter 5: The Untyped Lambda-Calculus

Figure 5-1: The Predecessor Function's "Inner Loop"

Figure 5-2: Evaluation of factorial c₃

Figure 5-3: Untyped Lambda-Calculus (λ)

Chapter 8: Typed Arithmetic Expressions

Figure 8-1: Typing Rules for Booleans (B)

Figure 8-2: Typing Rules for Numbers (NB)

Chapter 9: Simply Typed Lambda-Calculus

Figure 9-1: Pure Simply Typed Lambda-Calculus (λ→)

Chapter 11: Simple Extensions

Figure 11-1: Uninterpreted Base Types

Figure 11-2: Unit Type

Figure 11-3: Ascription

Figure 11-4: Let Binding

Figure 11-5: Pairs

Figure 11-6: Tuples

Figure 11-7: Records

Figure 11-8: (Untyped) Record Patterns

Figure 11-9: Sums

Figure 11-10: Sums (With Unique Typing)

Figure 11-11: Variants

Figure 11-12: General Recursion

Figure 11-13: Lists

Chapter 13: References

Figure 13-1: References

Chapter 14: Exceptions

Figure 14-1: Errors

Figure 14-2: Error Handling

Figure 14-3: Exceptions Carrying Values

Chapter 15: Subtyping

Figure 15-1: Simply Typed Lambda-Calculus with Subtyping (λ_<:)

Figure 15-2: Records (Same as Figure 11-7)

Figure 15-3: Records and Subtyping

Figure 15-4: Bottom Type

Figure 15-5: Variants and Subtyping

Chapter 16: Metatheory of Subtyping

Figure 16-1: Subtype Relation with Records (Compact Version)

Figure 16-2: Algorithmic Subtyping

Figure 16-3: Algorithmic Typing

Chapter 19: Case Study: Featherweight Java

Figure 19-1: Featherweight Java (Syntax and Subtyping)

Figure 19-2: Featherweight Java (Auxiliary Definitions)

Figure 19-3: Featherweight Java (Evaluation)

Figure 19-4: Featherweight Java (Typing)

Chapter 20: Recursive Types

Figure 20-1: Iso-Recursive Types (λμ)

Chapter 21: Metatheory of Recursive Types

Figure 21-1: Sample Tree Types.

Figure 21-2: A Sample Support Function

Figure 21-3: Sample treeof Application

Figure 21-4: Concrete Subtyping Algorithm for μ-Types

21-5: Amadio and Cardelli's Subtyping Algorithm

Chapter 22: Type Reconstruction

Figure 22-1: Constraint Typing Rules

Figure 22-2: Unification Algorithm

Chapter 23: Universal Types

Figure 23-1: Polymorphic Lambda-Calculus (System F)

Chapter 24: Existential Types

Figure 24-1: Existential Types

Chapter 26: Bounded Quantification

Figure 26-1: Bounded Quantification (Kernel F_<:)

Figure 26-2: "Full" Bounded Quantification

Figure 26-3: Bounded Existential Quantification (Kernel Variant)

Chapter 28: Metatheory of Bounded Quantification

Figure 28-1: Exposure Algorithm for F_<:

Figure 28-2: Algorithmic Typing for F_<:

Figure 28-3: Algorithmic Subtyping for Kernel F_<:

Figure 28-4: Algorithmic Subtyping for Full F_<:

Figure 28-5: Join and Meet Algorithms for Kernel F_<:

Chapter 29: Type Operators and Kinding

Figure 29-1: Type Operators and Kinding (λ_ω)

Chapter 30: Higher-Order Polymorphism

Figure 30-1: Higher-Order Polymorphic Lambda-Calculus (F_ω)

Figure 30-2: Higher-Order Existential Types

Figure 30-3: Parallel reduction on types

Chapter 31: Higher-Order Subtyping

Figure 31-1: Higher-Order Bounded Quantification ()

Chapter 32: Case Study: Purely Functional Objects

Figure 32-1: Polymorphic Update

Appendix A: Solutions to Selected Exercises

Figure A-1: Typed Record Patterns

Figure A-2: Minimal X-Free Supertype and Maximal X-Free Subtype of a Given Type

---