Types and Programming Languages

[delta4d]

Preface

• [x] Introduction
• [x] Mathematical Preliminaries

  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

  Simple Types

• [ ] Typed Arithmetic Expressions
• [ ] Simply Typed Lambda-Calculus
• [ ] An ML Implementation of Simple Types
• [ ] Simple Extensions
• [ ] Normalization
• [ ] References
• [ ] Exceptions

  Subtyping

• [ ] Subtyping
• [ ] Metatheory of Subtyping
• [ ] An ML Implementation of Subtyping
• [ ] Case Study: Imperative Objects
• [ ] Case Study: Featherweight Java

  Recursive Types

• [ ] Recursive Types
• [ ] Metatheory of Recursive Types

  Polymorphism

• [ ] Type Reconstruction
• [ ] Universal Types
• [ ] Existential Types
• [ ] An ML Implementation of System F
• [ ] Bounded Quantification
• [ ] Case Study: Imperative Objects, Redux
• [ ] Metatheory of Bounded Quantification

  Higher-Order Systems

• [ ] Type Operators and Kinding
• [ ] Higher-Order Polymorphism
• [ ] Higher-Order Subtyping
• [ ] Case Study: Purely Functional Objects

[delta4d]

Introduction

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

[delta4d]

Mathematical Preliminaries

Set

Relation

Function