Wir haben den einfach getypten λ-Kalkül und ein paar selektive Erweiterungen kennengelernt. Wir haben damit schon einiges von dem Werkzeug, was man benötigt um eine richtige Programmiersprache zu beschreiben. Was zu einer richtigen Sprache noch fehlt sind vernünftig definierte Basisdatentypen und Funktionen auf ihnen (z.B. Zahlen und Rechenoperationen) sowie Konstrukte um rekursive Funktionen und Datentypen definieren zu können.
Als sinnvolle Erweiterungen am einfach getypten λ-Kalkül könnte man noch Varianten (ähnlich wie unions in C) und allgemeine k-Tupel betrachten.
Die Ausdruckskraft eines Typsystems steigt erheblich, sobald man polymorphe Datentypen mit Typparametern hinzufügt. Die mächtigsten in der Informatik gebräuchlich Typsystem (beispielsweise Fω) heben praktisch den gesamten einfach getypten λ-Kalkül eine Ebene nach oben, definieren also Funktionsabstraktion und Applikation auf der Ebenen von Typen (statt Termen).
Der Sourcecode für die Sprache mit den Boolschen Ausdrücken ist hier.
Der Sourcecode für den ungetypten λ-Kalkül ist hier.
Der Sourcecode für den einfach getypen λ-Kalkül ist hier.
Alle Sourcen enthalten unten ein paar Beispielterme zum rumprobieren.
Im wesentlichen ist das Buch Types and Programming Languages von Benjamin C. Pierce zu nennen.
Den Überblick über die verschiedenen Semantiken (Übersetzersemantik, operationale Semantik, denotationale Semantik und axiomatische Semantik) habe ich dem Duden der Informatik entnommen.
Online können Unterlagen zu den Themen λ-Kalkül und operationale Semantiken aus dem Informatikseminar WS04/05 bezogen werden. Dort findet sich auch ein Vortrag über Statische Typüberprüfung am Beispiel von Haskell (und ML).
Den Wikipedia-Artikel http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus über den einfach getypten λ-Kalkül kann ich zum jetzigen Zeitpunkt (15.12.2005) nicht empfehlen. (Sehr technisch. Scheint für Informatiker nicht geeignet. Für Mathematiker: Ich kann es nicht beurteilen.)