Erweiterungen, Anwendungen

ausgehend vom einfachen Lambda-Kalkül baut man:

• Typsysteme (jeder Ausdruck, jede Variable besitzt Typ)
• eingebaute Datentypen (außer Funktionen) und Operationen, z. B. Zahlen
• effiziente Implementierung von Reduktionen (ohne die umständlichen Umbenennungen)

das bildet die Grundlage für

• exakte Analyse von Programmier/mathematischen/logischen Sprachen
• Implementierung von Sprachen und Refactoring-Werkzeugen