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?