Modeling objects (OOP) in dependent type theory 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?
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.