Practical Foundations for Programming Languages 1

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