I Judgements and Rules

• Abstract Syntax
• Inductive Difintions
• Hypothetical and General Judgements

II Statics and Dynamics

• Statics
• Dynamics
• Type Safety
• Evaluation Dynamics

III Total Functions

• Function Definitions and Values
• System T

IV Finite Data Types

• Product Types
• Sum Types

V Types and Propositions

• Constructive Logic
• Classical Logic

1 Abstract Syntax

2 Inductive Difintions

3 Hypothetical and General Judgements

4 Statics

5 Dynamics

6 Type Safety

7 Evaluation Dynamics

8 Function Definitions and Values

9 System T

10 Product Types

11 Sum Types

12 Constructive Logic

13 Classical Logic