alpha_calculus

Formalization and proofs for a language extending lambda calculus.

Features

• Built in types
  • Integers
  • Booleans
• Fix point of functions (recursion)
• let bindings
• Product types (n-tuples)

Proofs

• Type preservation
• Progress
• Interpreter correctness
• Inference correctness
• Well-foundedness of types