Download: PDF.

“Ownership Type Systems and Dependent Classes” by W. Dietl and P. Müller. In Foundations of Object-Oriented Languages (FOOL), Jan. 2008.


Ownership type systems structure the heap and enforce restrictions on the behavior of a program. Benefits of ownership type systems include simplified program verification, absence of race conditions and deadlocks, and enforcement of architectural styles.

Dependent classes are a generalization of virtual class systems that allows one class to depend on multiple objects. Dependency is expressed by explicit declaration of the depended-upon objects as class parameters. This allows one to declare dependencies independently of the nesting of classes, which increases the expressive power and reduces the coupling between classes.

In this paper, we describe how ownership type systems can be expressed on top of dependent classes. The ownership type systems are split into two parts: (1) ensuring the topological structure of the heap and (2) enforcing restrictions on the behavior of the program. We present an encoding of the topological part in dependent classes and describe how to enforce the restrictions of ownership type systems directly on the dependent classes program. Finally, we present the encoding of some examples for the MVC interpreter and discuss future work.

Download: PDF.

BibTeX entry:

   author = {W. Dietl and P. M{"u}ller},
   title = {{Ownership Type Systems and Dependent Classes}},
   booktitle = {Foundations of Object-Oriented Languages (FOOL)},
   month = jan,

Back to the publications by date or by topic.

(This webpage was created with bibtex2web.)