Typsysteme für Programmiersprachen

Strenges Typisieren verhindert nicht nur Fehler, sondern trägt (bereits in der Entwurfsphase) zur Klarheit der Software bei. Der Typ eines Bezeichners ist seine beste Dokumentation!

Typsysteme beschleunigen Programme: der Compiler kann Typinformationen benutzen, um effizienten (d. h. spezialisierten) Code zu generieren.

Bei Entwurf und Anwendung eines Typsystems balanciert man zwischen

• Ausdrucksstärke: alle "sinnvollen" Funktionen, Datentypen, und Abstraktionen davon (!) sollen auch typisierbar sein (aber alle "unsinnigen" nicht)
• und Effektivität: wichtige Fragen (hat der Term x den Typ t?) sollen effektiv entscheidbar sein.

Ich gebe "für die Theoretiker" einen Überblick über Ziele, Ansätze, Stärken und Schwächen von Typsystemen in realen (imperativen, objekt-orientierten und funktionalen) Programmiersprachen.

Gleichzeitig erläutere ich "für die Praktiker" den notwendigen mathematischen Hintergrund, insbesondere verschiedene Erweiterungen des einfach getypten Lambda-Kalküls.

Der Vortrag spricht damit einen breites Publikum an, Gäste sind herzlich eingeladen.

Literatur:

• Martin Abadi und Luca Cardelli: A Theory of Objects, http://www.luca.demon.co.uk/TheoryOfObjects.html
• Henk Barendregt: Lambda Calculi with Types, in: Handbook of Logic in Computer Science, auch: ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z
• Benjamin C. Pierce: Types and Programming Languages, http://www.cis.upenn.edu/~bcpierce/tapl/main.html