<p>There is a substantially expanded follow paper Andreas Abel, Stephan Adelsberger, Anton Setzer: <a href="http://www.cs.swan.ac.uk/~csetzer/articles/ooAgda.pdf" rel="nofollow noreferrer">Interactive Programming in Agda - 
Objects and Graphical User Interfaces</a>. It contains an <a href="https://github.com/agda/ooAgda" rel="nofollow noreferrer">Agda library</a> 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.</p>

CC BY-SA 4.0
2018-12-14T12:12:52.790Z
2018-12-14T12:12:52.790Z
Anton Setzer
<p>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, <a href="https://www.cs.rhul.ac.uk/~seokhyun/" rel="nofollow"><em>Verification of Java Programs in Type Theory with Dependent Record Types and Coercive Subtyping</em></a>.</p>

<p>Some <a href="https://www.itu.dk/people/jobr/itp2011.pdf" rel="nofollow">recent work on separation logic</a> also seems relevant.</p>

CC BY-SA 3.0
2011-12-22T22:25:48.753Z
2011-12-22T22:25:48.753Z
Francois G
<p>Why are you looking at <em>dependent</em> 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.</p>

<p>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.</p>

<p>Maybe you want to give a finer static semantics to OOP constructs that
are currently untyped, such as <code>instance_of</code> followed by
a <code>cast</code>. 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.</p>

CC BY-SA 3.0
2011-12-23T10:23:13.663Z
This is not an answer to the question. This isn't a discussion forum.
Dave Clarke
CC BY-SA 3.0
2011-12-23T09:28:55.383Z
2011-12-23T09:28:55.383Z
gasche
<p>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 <a href="http://wwwhome.ewi.utwente.nl/~marieke/papers.html" rel="noreferrer">publication page</a> 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.</p>

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

<p>There is a workshop series known as <a href="http://www.cs.ru.nl/ftfjp/" rel="noreferrer">FTfJP</a> (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.</p>

CC BY-SA 3.0
2011-12-23T08:50:39.977Z
2011-12-23T08:50:39.977Z
Dave Clarke
<p>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.</p>

<p>I could only find one Paper on modeling objects in dependent type theory, which is:<br>
<a href="http://www.cs.swan.ac.uk/~csetzer/articles/objectOrientedProgrammingInDepTypeTheoryTfp2006PostProceedings.pdf">Object-oriented programming in dependent type theory by A. Setzer (2006)</a></p>

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

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

<reference-request><pl.programming-languages><type-theory><coq><dependent-type>
Modeling objects (OOP) in dependent type theory
mrsteve
# Modeling objects (OOP) in dependent type theory

(Asked by: username_0 on 2011-12-22)

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)](http://www.cs.swan.ac.uk/~csetzer/articles/objectOrientedProgrammingInDepTypeTheoryTfp2006PostProceedings.pdf)

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?

**Tags:** reference-request, pl.programming-languages, type-theory, coq, dependent-type


---

## 4 answers

### Answer by username_4 on 2011-12-23. Score: 6 | Accepted answer

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](http://wwwhome.ewi.utwente.nl/~marieke/papers.html) 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](http://www.cs.ru.nl/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 by username_1 on 2018-12-14. Score: 3

There is a substantially expanded follow paper Andreas Abel, Stephan Adelsberger, username_1: [Interactive Programming in Agda -
Objects and Graphical User Interfaces](http://www.cs.swan.ac.uk/~csetzer/articles/ooAgda.pdf). It contains an [Agda library](https://github.com/agda/ooAgda) 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 by username_2 on 2011-12-22. Score: 2

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*](https://www.cs.rhul.ac.uk/~seokhyun/).

Some [recent work on separation logic](https://www.itu.dk/people/jobr/itp2011.pdf) also seems relevant.


---

### Answer by username_3 on 2011-12-23. Score: 2

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.

> **Comments:**
> **username_4**: This is not an answer to the question. This isn't a discussion forum.  

---

