Typsysteme für statische Programmiersprachen sollen die Abwesenheit von Typfehlern in Quellcode prüfen, bevor ein Programm ausgeführt wird. Typsysteme, die diese Erwartung erfüllen, werden in der Literatur als korrekte Typsysteme bezeichnet. In der Praxis sind viele Typsysteme allerdings nicht korrekt, d.h. sie akzeptieren unter Umständen Programme mit Typfehlern, die während der Ausführung zu undefiniertem Verhalten führen. Um verlässlich die Korrektheit eines Typsystems sicherzustellen schlägt ein Untergebiet in der Forschung zu Programmiersprachen vor, Korrektheitsbeweise von Typsystemen zu entwickeln: Man beweist formal eine Korrektheitseigenschaft für eine logische Spezifikation eines Typsystems mit Hilfe von logischen Schlussfolgerungen. Die Mechanisierung eines solchen Beweises soll sicherstellen, dass der Beweis keine menschengemachten Schlussfolgerungsfehler enthält: Ein Verifikationssystem überprüft, ob alle Schritte in einem Beweis korrekt im Hinblick auf die Regeln der verwendeten Logik sind.

Allerdings ist die Entwicklung von mechanisierten Korrektheitsbeweisen für Typsysteme mit Hilfe heutiger Methodik und heute verfügbaren Werkzeugen selbst für Experten im Bereich der formalen Verifikation eine äußerst aufwendige Aufgabe: Heute verfügbare Werkzeuge erfordern oft, dass eine große Anzahl "trivialer" Beweisschritte manuell ausformuliert werden, was ein gewisses Level an Fähigkeiten und Expertise im Gebiet der formalen Verifikation erfordert. Entwickler von Programmiersprachen sowie Forscher, die Experten darin sind, wie man Korrektheitsbeweise von Typsystemen auf dem Papier durchführt, sind oft nicht gleichzeitig versiert im Umgang mit Werkzeugen für mechanisierte Verifikation. Solche Entwickler und Forscher sind typischerweise schnell frustriert angesichts des nötigen Aufwands für mechanisierte Verifikation und verfolgen daher die Mechanisierung ihrer Beweise oft nicht weiter.

Das Hauptziel dieser Arbeit besteht darin, den Automatisierungsgrad für die Mechanisierung von Korrektheitsbeweisen für Typsysteme zu erhöhen. Hierfür studieren wir zunächst existierende Arbeiten zur Mechanisierung solcher Beweise aus der Literatur. Wir verwenden unsere Beobachtungen hierzu auf der einen Seite, um die Menge der Programmiersprachen, die wir in dieser Arbeit betrachten, einzuschränken: Wir beschränken uns auf domänenspezifische Programmiersprachen (DSLs) ohne vollwertige Konstrukte zum Binden von abstrakten Namen. Auf der anderen Seite verwenden wir unsere Beobachtungen um zu identifizieren, welche generellen Schwächen existierende Verifikationssysteme besitzen, wenn es darum geht, Experten in verschiedenen Verifikationsdomänen darin zu unterstützen, domänenspezifische, automatische Beweisstrategien innerhalb ihrer Domäne zu entwickeln.

Auf der Basis unserer Beobachtungen schlagen wir eine generische Verifikationsinfrastruktur namens VeriTaS für die Automatisierung von domänenspezifischen Verifikationsaufgaben vor: VeriTaS ist eine leichtgewichtige Programmierbibliothek in Scala um automatische, domänenspezifische Beweisstrategien für die Generierung von Hauptschritten von Beweisen mit existierenden automatischen Theorembeweisern zu kombinieren, welche einzelne, technische Beweisschritte verifizieren. VeriTaS ist generisch in einem Eingabeformat für Problemspezifikationen. Daher kann die Infrastruktur für verschiedene Verifikationsdomänen instanziiert werden.

Wir instanziieren unsere VeriTaS-Verifikationsinfrastruktur für die Generierung von Korrektheitsbeweisen für Typsysteme von DSLs: Wir stellen ein domänenspezifisches Eingabeformat für Typsystemspezifikationen sowie Basistaktiken bereit, welche einzelne detaillierte Beweisschritte erstellen. Außerdem präsentieren wir automatische Beweisstrategien zur Generierung von Beweisstrukturen für Korrektheitsbeweise von Typsysteme. Wir evaluieren unsere Beweisstrategien anhand von zwei Fallstudien, beides Typsysteme von repräsentativen DSLs. Zusätzlich führen wir eine empirische Studie durch, um verschiedene Enkodierungsstrategien für Beweisprobleme auf Detailebene miteinander zu vergleichen. Die Ergebnisse unserer Studie haben wir dazu verwendet, den Automatisierungsgrad unserer Beweisstrategien für Korrektheitsbeweise von Typsystemen in VeriTaS weiter zu erhöhen.

Unsere Fallstudien zeigen, dass unsere Instanziierung von VeriTaS für Korrektheitsbeweise von Typsystemen von DSLs einen höheren Automatisierungsgrad für solche Beweise erreicht als existierende Systeme.