lambda-cube

Features

• All typed languages are Church style with explicit type-annotations.

Roadmap / Todo

• Untyped Lambda Calculus
  • Normal Order
  • Applicative Order
  • Call by name
  • Call by need
  • README
• Simply Typed Lambda Calculus
• System F
  • Type alias
  • Pairs / Product
• System F Omega
• Lambda Pi
  • Not implemented yet
• Calculus of constructions
  • Not implemented yet