Library TAPL.UntypedArithExpr

Library TAPL.ArithExpr

• ArithExpr: The Typed Calculus of Booleans and Numbers
  • Types
  • Terms
  • Values
  • Small-step Operational Semantics
  • Small-step semantics
  • Properties of Evaluation
  • Multi-step Evaluation
  • Multi-step Evaluation
  • Big-step Evaluation
  • Relationship between Big-step and Small-step
  • Type Checking
  • Type Safety: Type Preservation and Progress

Library TAPL.Stlc

• Stlc: The Simply Typed Lambda-Calculus
• Syntax
• Operational Semantics
• Typing
• Type Safety Properties