Twelf ist eine Sprache, mit der man deduktive Systeme wie Programmiersprachen und Logiken festlegen, umsetzen und ihre Eigenschaften beweisen kann. Sie ist zugleich Programmiersprache und Beweiswerkzeug. Finden Sie mehr rund ums Programmieren auf unserer Schwerpunktseite Programmiersprachen.
Geschichte
Twelf ist laut Projektseite ein Forschungsprojekt zu Entwurf, Umsetzung und Anwendung logischer Frameworks. Gefördert wurde es von der National Science Foundation, unter anderem mit Frank Pfenning als leitendem Forscher, und von der DARPA im Rahmen des Fox Project, das Robert Harper, Peter Lee und Frank Pfenning leiteten. Hauptautoren von Twelf sind Frank Pfenning und Carsten Schürmann; wichtige Beiträge kamen von Brigitte Pientka, Roberto Virga und Kevin Watkins. Laut Website wird Twelf heute nicht mehr aktiv weiterentwickelt, hat aber weiterhin eine Nutzergemeinschaft und bleibt ein wertvolles Forschungswerkzeug.
Merkmale
Die Umsetzung umfasst das logische Framework LF mit Typrekonstruktion, die Constraint-Logikprogrammiersprache Elf, einen noch sehr vorläufigen induktiven Beweiser für Metatheoreme über LF und eine Oberfläche für den Editor Emacs. Zu den Beispielen gehören der Church-Rosser-Satz für den ungetypten Lambda-Kalkül und Mini-ML mit Typerhaltung und Übersetzung. Größere Forschungsprojekte mit Twelf sind laut Website die getypte Assemblersprache TALT, ein System für beweistragenden Code und ein Beweis der Typsicherheit von Standard ML.
Einordnung
Twelf gehört zu den Werkzeugen für die formale Theorie der Programmiersprachen. Ein Werkzeug zur formalen Spezifikation von Systemen ist TLA+. Weitere Sprachen finden Sie in unserer Liste: Programmiersprachen, die mit T beginnen.
Quellen
Stand: 15.10.2026