---

Download: PDF.

“Comparing Universes and Existential Ownership Types” by N. Cameron and W. Dietl, School of Engineering and Computer Science. VUW technical report 06, July 2009. https://ecs.victoria.ac.nz/twiki/pub/Main/TechnicalReportSeries/ECSTR09-06.pdf.

Abstract

Ownership types and Universe types are two type systems used to structure the heap and enforce encapsulation disciplines. The parametricity of ownership types allows a finer-grained description of heap topologies, whereas the flexibility of any references in Universe types allows sharing between data structures. No direct encoding of one type system in the other has been possible.

Parametric ownership has recently been extended with existential quantification of contexts. We formalise such a language and give a formal translation between programs written in this language and using Universe types. We show that this translation is sound and complete.

Keywords: JoE, UTS

Download: PDF.

BibTeX entry:

@techreport{CameronDietl09a,
   author = {N. Cameron and W. Dietl},
   title = {{Comparing Universes and Existential Ownership Types}},
   institution = {School of Engineering and Computer Science, VUW},
   month = jul,
   note =
}

---

---