Lambda language

Lambda is a language inspired by some mathematics notations and mostly influenced by the functional programming paradigm with a focus on extending typed lambda calculus.

The language supports many levels of programming as type level and value level. It is designed to be a functional lambda calculus language with a strong type system while keeping a pleasant and logical syntax.

Summary

Language implementation specifications

• Parsing Lambda language
• Abstract tree elements definitions
• Type system
• Interpretation step
  • Typechecking values
  • Kind-checking types
  • Evaluating value expressions
  • Evaluating type expressions
• Optimizations
• Type inference rules

User applications

• Type level programming introduction
• Real world use-cases of type level
• Some theoretical examples
• Using Lambda as a theorem prover

Examples

• Recursive factorial for ℕ