Modelowanie obiektów (OOP) w teorii typów zależnych

Interesuje mnie modelowanie obiektów, od programowania obiektowego, w teorii typów zależnych. Jako możliwą aplikację chciałbym mieć model, w którym mogę opisać różne cechy imperatywnych języków programowania.

Znalazłem tylko jeden artykuł na temat modelowania obiektów w teorii typów zależnych, a mianowicie :
Programowanie obiektowe w teorii typów zależnych A. Setzer (2006)

Czy są jakieś dalsze odniesienia na ten temat, które przegapiłem i być może są nowsze?

Czy może istnieje implementacja (tj. Dowód) dla dowodu twierdzenia, takiego jak Coq lub Agda?

Niektóre wczesne (?) Prace wykonane w tym obszarze wykonali Bart Jacobs (Nijmegen) i Marieke Huisman. Ich praca opiera się na narzędziu PVS i opierała się na kodowaniu klasowym (jeśli dobrze pamiętam). Zajrzyj na stronę publikacji Marieke z artykułami z 2000 roku i jej pracę doktorską w 2001 roku. Zobacz także artykuły Barta Jacobsa cytowane w artykule A Setzer, o którym wspominałeś.

W tamtych czasach mieli coś, co nazywało się narzędziem LOOP, ale wydaje się, że zniknęło z Internetu.

Istnieje seria warsztatów znana jako FTfJP (Formal Techniques for Java-podobnych programów), która dotyczy formalnej weryfikacji programów OO. Niewątpliwie część pracy wykorzystuje zależną teorię typów / logikę wyższego rzędu. Seria warsztatów trwa od około 14 lat.

Istnieje znacznie rozszerzony artykuł śledzący Andreas Abel, Stephan Adelsberger, Anton Setzer: Programowanie interaktywne w Agda - Obiekty i graficzne interfejsy użytkownika . Zawiera bibliotekę Agda do pisania programów obiektowych, w tym GUI. Istnieje kilka prac uzupełniających ze Stephanem Adelsbergerem na temat pisania zweryfikowanych GUI w domenie medycznej w Agda w oparciu o programowanie obiektowe.

Nie jestem wystarczająco dobrze zaznajomiony z tym tematem, aby dać przyzwoity przegląd, ale radziłbym, aby przejrzeć bibliografię pod koniec 2010 r. Pracy doktorskiej Seokhyun Han, Weryfikacja programów Java w teorii typów z zależnymi typami rekordów i przymusowym subtypingiem .

Istotne wydają się również niektóre ostatnie prace nad logiką separacji .

Dlaczego patrzysz na teorię typów zależnych do reprezentowania OOP? Czy nie możemy modelować OOP w zadowalający sposób za pomocą niezależnych rachunków? Mam nieformalny model tego, jak wygląda OOP, powiedzmy, po przetłumaczeniu na system F (lub Fω, jeśli chcesz obsługiwać generyczne), i nie widzę, gdzie miałaby zastosowanie zależność od wartości typu.

Typy zależne mogą być używane, na przykład, do nadania niższego poziomu znaczenia algebraicznym typom danych. Prawdopodobnie możesz wykonać takie niskopoziomowe kodowanie funkcji OO, ale nie jestem pewien, czy to lepsze niż dodanie algebraicznych typów danych do języka modelowania.

Być może chcesz nadać bardziej precyzyjną semantykę statyczną konstruktom OOP, które są obecnie bez typu, na przykład instance_ofpo którym następuje cast. Widzę, że hackery typu zależnego są przydatne do statycznego uzasadnienia takich programów; ale nie jestem pewien, czy „modelowałoby” te operacje, które koncentrują się na kącie dynamicznym, to coś więcej.