Objetos de modelado (OOP) en la teoría del tipo dependiente

13

Estoy interesado en modelar objetos, desde la programación orientada a objetos, en la teoría del tipo dependiente. Como posible aplicación, me gustaría tener un modelo donde pueda describir diferentes características de los lenguajes de programación imperativos.

Solo pude encontrar un artículo sobre modelos de objetos en la teoría de tipos dependientes, que es:
Programación orientada a objetos en teoría de tipos dependientes por A. Setzer (2006)

¿Hay más referencias sobre el tema que me perdí y quizás hay más recientes?

¿Existe quizás una implementación (es decir, una prueba) disponible para un probador de teoremas, como Coq o Agda?

mrsteve
fuente

Respuestas:

6

Algunos trabajos tempranos (?) Realizados en esta área fueron realizados por Bart Jacobs (Nijmegen) y Marieke Huisman. Su trabajo se basa en la herramienta PVS y se basa en una codificación coalgebraic de clases (si no recuerdo mal). Mire la página de publicación de Marieke para los trabajos en el año 2000 y su tesis doctoral en 2001. También mire los trabajos de Bart Jacobs citados en el artículo de A Setzer que menciona.

En aquellos días, tenían algo llamado la herramienta LOOP, pero parece haber desaparecido de Internet.

Hay una serie de talleres conocida como FTfJP (Técnicas formales para programas similares a Java) que aborda la verificación formal de los programas OO. Indudablemente, parte del trabajo utiliza la teoría del tipo dependiente / lógica de orden superior. La serie de talleres ha estado funcionando durante unos 14 años.

Dave Clarke
fuente
2

¿Por qué estás mirando la teoría del tipo dependiente para representar OOP? ¿No podemos modelar OOP de una manera satisfactoria con cálculos no dependientes? Tengo un modelo informal de cómo se ve OOP, por ejemplo, cuando se traduce al Sistema F (o Fω si desea admitir genéricos), y no veo dónde entraría en juego la dependencia del valor de tipo.

Los tipos dependientes pueden usarse, por ejemplo, para dar un significado de nivel inferior a los tipos de datos algebraicos. Probablemente podría hacer una codificación de tan bajo nivel de características OO, pero no estoy seguro de que sea mejor que agregar tipos de datos algebraicos a su lenguaje de modelado.

Tal vez desee dar una semántica estática más fina a las construcciones de OOP que actualmente no están tipificadas, como las instance_ofseguidas de a cast. Puedo ver que la piratería de tipo dependiente es útil para razonar estáticamente sobre tales programas; pero no estoy seguro de que "modele" esas operaciones que se concentran en el ángulo dinámico, es algo más.

gasche
fuente
Esta no es una respuesta a la pregunta. Este no es un foro de discusión.
Dave Clarke