Modeling objects (OOP) in dependent type theory

Question

I am interested in modeling objects, from object oriented programming, in dependent type theory. As a possible application, I would like to have a model where I can describe different features of imperative programming languages.

I could only find one Paper on modeling objects in dependent type theory, which is:
Object-oriented programming in dependent type theory by A. Setzer (2006)

Are there further references on the topic that I missed and perhaps are there more recent ones?

Is there perhaps an implementation (i.e. proof) available for a theorem prover, like Coq or Agda?

Answer 1

Some early(?) work done in this area was by Bart Jacobs (Nijmegen) and Marieke Huisman. Their work is based on the PVS tool and relied on a coalgebraic encoding of classes (if I remember correctly). Look at Marieke's publication page for papers in the year 2000 and her PhD thesis in 2001. Also look at the papers by Bart Jacobs cited in the A Setzer paper you mention.

Back in those days, they had something called the LOOP tool, but it seems to have vanished from the internets.

There is a workshop series known as FTfJP (Formal Techniques for Java-like Programs) that addresses the formal verification of OO programs. Undoubtedly some of the work uses dependent type theory/higher-order logic. The workshop series has been running for some 14 years.

Answer 2

There is a substantially expanded follow paper Andreas Abel, Stephan Adelsberger, Anton Setzer: Interactive Programming in Agda - Objects and Graphical User Interfaces. It contains an Agda library for writing object-based programs, inluding GUIs. There are some follow up papers with Stephan Adelsberger on writing verified GUIs in the medical domain in Agda based on object-oriented programming.

Answer 3

I am not well-versed enough in the subject to give a decent overview, but I would advise to scavenge the bibliography of the late 2010 PhD thesis of Seokhyun Han, Verification of Java Programs in Type Theory with Dependent Record Types and Coercive Subtyping.

Some recent work on separation logic also seems relevant.

Answer 4

Why are you looking at dependent type theory to represent OOP? Can't we model OOP in a satisfying way with non-dependent calculi? I have an informal model of what OOP looks like, say, when translated to System F (or Fω if you want to support generics), and I don't see where the type-value dependency would come into play.

Dependent types can be used, for example, to give a lower-level meaning to algebraic data types. You could probably do such a low-level encoding of OO features, but I'm not sure that's better than adding algebraic datatypes to your modeling language.

Maybe you want to give a finer static semantics to OOP constructs that are currently untyped, such as instance_of followed by a cast. I can see dependent type hackery being useful to statically reason about such programs; but I'm not sure it would "model" those operations that concentrate on the dynamic angle, it's something more.