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?