Modelagem de objetos (OOP) na teoria de tipos dependentes

Estou interessado em modelar objetos, a partir de programação orientada a objetos, na teoria dos tipos dependentes. Como possível aplicação, eu gostaria de ter um modelo em que possa descrever diferentes recursos de linguagens de programação imperativas.

Eu só consegui encontrar um artigo sobre modelagem de objetos na teoria dos tipos dependentes, que é:
Programação orientada a objetos na teoria dos tipos dependentes por A. Setzer (2006)

Existem outras referências sobre o assunto que eu perdi e talvez outras mais recentes?

Existe talvez uma implementação (ou seja, prova) disponível para um provador de teoremas, como Coq ou Agda?

Alguns dos primeiros trabalhos realizados nesta área foram por Bart Jacobs (Nijmegen) e Marieke Huisman. Seu trabalho é baseado na ferramenta PVS e contava com uma codificação coalgebraica de classes (se bem me lembro). Veja a página de publicação de Marieke para artigos no ano 2000 e sua tese de doutorado em 2001. Veja também os artigos de Bart Jacobs citados no artigo A Setzer que você mencionou.

Naquela época, eles tinham algo chamado de ferramenta LOOP, mas parece ter desaparecido das Internet.

Há uma série de workshops conhecida como FTfJP (Técnicas formais para programas semelhantes a Java) que aborda a verificação formal de programas OO. Sem dúvida, parte do trabalho utiliza a teoria dos tipos dependentes / lógica de ordem superior. A série de workshops já dura 14 anos.

Há um artigo de acompanhamento substancialmente expandido: Andreas Abel, Stephan Adelsberger e Anton Setzer: Programação Interativa em Agda - Objetos e Interfaces Gráficas de Usuário . Ele contém uma biblioteca Agda para escrever programas baseados em objetos, incluindo GUIs. Existem alguns documentos de acompanhamento com Stephan Adelsberger sobre a criação de GUIs verificadas no domínio médico na Agda, com base na programação orientada a objetos.

Não sou suficientemente versado no assunto para fornecer uma visão geral decente, mas aconselho a vasculhar a bibliografia da tese de doutorado de Seokhyun Han de 2010, verificação de programas Java em teoria de tipos com tipos de registros dependentes e subtipos coercitivos .

Alguns trabalhos recentes sobre lógica de separação também parecem relevantes.

Por que você está analisando a teoria dos tipos dependentes para representar OOP? Não podemos modelar a POO de maneira satisfatória com cálculos não dependentes? Eu tenho um modelo informal de como o OOP se parece, digamos, quando traduzido para o Sistema F (ou Fω se você deseja oferecer suporte a genéricos), e não vejo onde a dependência do tipo de valor entraria em jogo.

Tipos dependentes podem ser usados, por exemplo, para dar um significado de nível inferior aos tipos de dados algébricos. Você provavelmente poderia fazer uma codificação de baixo nível dos recursos de OO, mas não tenho certeza se isso é melhor do que adicionar tipos de dados algébricos à sua linguagem de modelagem.

Talvez você queira fornecer uma semântica estática mais refinada para construções OOP que atualmente não são tipadas, como instance_ofseguidas por a cast. Vejo hackery de tipo dependente sendo útil para raciocinar estaticamente sobre esses programas; mas não tenho certeza de que "modelaria" essas operações que se concentram no ângulo dinâmico, é algo mais.