Modellieren von Objekten (OOP) in der Theorie abhängiger Typen

Ich interessiere mich für die Modellierung von Objekten aus der objektorientierten Programmierung in der Theorie der abhängigen Typen. Als mögliche Anwendung hätte ich gerne ein Modell, in dem ich verschiedene Funktionen von imperativen Programmiersprachen beschreiben kann.

Ich konnte nur einen Artikel zur Modellierung von Objekten in der Theorie abhängiger Typen finden, nämlich:
Objektorientierte Programmierung in der Theorie abhängiger Typen von A. Setzer (2006)

Gibt es weitere Referenzen zu dem Thema, die ich verpasst habe und vielleicht neuere?

Gibt es vielleicht eine Implementierung (dh einen Beweis) für einen Theorembeweiser wie Coq oder Agda?

Einige frühe (?) Arbeiten in diesem Bereich wurden von Bart Jacobs (Nijmegen) und Marieke Huisman ausgeführt. Ihre Arbeit basiert auf dem PVS-Tool und basiert auf einer kohlebraischen Codierung von Klassen (wenn ich mich richtig erinnere). Schauen Sie sich die Veröffentlichungsseite von Marieke für Arbeiten aus dem Jahr 2000 und ihre Doktorarbeit aus dem Jahr 2001 an. Schauen Sie sich auch die Arbeiten von Bart Jacobs an, die in der von Ihnen erwähnten A Setzer-Arbeit zitiert wurden.

Damals hatten sie das LOOP-Tool, aber es scheint aus dem Internet verschwunden zu sein.

Es gibt eine Workshop-Reihe namens FTfJP (Formal Techniques for Java-like Programs), die sich mit der formalen Verifizierung von OO-Programmen befasst. Zweifellos verwendet ein Teil der Arbeit eine abhängige Typentheorie / Logik höherer Ordnung. Die Workshop-Reihe läuft seit rund 14 Jahren.

Es gibt ein wesentlich erweitertes Folgepapier Andreas Abel, Stephan Adelsberger, Anton Setzer: Interaktive Programmierung in Agda - Objekten und grafischen Benutzeroberflächen . Es enthält eine Agda-Bibliothek zum Schreiben von objektbasierten Programmen, einschließlich GUIs. Mit Stephan Adelsberger gibt es einige Folgepapiere zum Verfassen von verifizierten GUIs im medizinischen Bereich in Agda, die auf objektorientierter Programmierung basieren.

Ich bin mit dem Thema nicht gut genug vertraut, um einen vernünftigen Überblick zu geben, aber ich würde raten, die Bibliographie der Doktorarbeit von Seokhyun Han Ende 2010, Überprüfung von Java-Programmen in der Typentheorie mit abhängigen Datensatztypen und Zwangssubtypisierung, zu überarbeiten .

Einige neuere Arbeiten zur Trennungslogik scheinen ebenfalls relevant zu sein.

Warum betrachten Sie die Theorie abhängiger Typen, um OOP darzustellen? Können wir OOP nicht auf zufriedenstellende Weise mit nicht abhängigen Kalkülen modellieren? Ich habe ein informelles Modell, wie OOP beispielsweise bei der Übersetzung in System F (oder Fω, wenn Sie Generika unterstützen möchten) aussieht, und ich sehe nicht, wo die Typ-Wert-Abhängigkeit ins Spiel kommen würde.

Abhängige Typen können beispielsweise verwendet werden, um algebraischen Datentypen eine niedrigere Bedeutung zu geben. Sie könnten wahrscheinlich eine so einfache Codierung von OO-Features durchführen, aber ich bin mir nicht sicher, ob dies besser ist, als Ihrer Modellierungssprache algebraische Datentypen hinzuzufügen.

Vielleicht möchten Sie OOP-Konstrukten, die derzeit nicht typisiert sind, eine feinere statische Semantik geben, z. B. instance_ofgefolgt von einem cast. Ich kann feststellen, dass abhängige Art von Hackery nützlich ist, um statisch über solche Programme nachzudenken. Aber ich bin nicht sicher, ob es diese Operationen "modellieren" würde, die sich auf den dynamischen Winkel konzentrieren. Es ist etwas mehr.