File PCF.Requirements

File PCF.Types

• Standard types
• More types

File PCF.Contexts

• Definition of Contexts
• Constructions on contexts
• Properties of contexts

File PCF.Formulas

• Definition of Formulas
• Operations and properties
  • Occurence of variables
  • Lifting
  • Substitution
• More formulas
  • Booleans
  • If-Then-Else

File PCF.Terms

• Derivable terms in context
• Properties of type derivation
• Derivation of defined formulas
• Some Examples
• The Faculty function in PCF
• The Maybe Monad: FX = X + 1

File PCF.CBN

• Values
• Big-Step Call-by-Name

File PCF.CBV

• Values
• Big-Step Call-by-Value